1 /-
2 Copyright (c) 2019 Jeremy Avigad. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Jeremy Avigad, Yury Kudryashov
5 -/
6
7 import analysis.normed_space.basic tactic.alias
src └─────────────────────────┘ └──────────┘
8
9 /-!
10 # Asymptotics
11
12 We introduce these relations:
13
14 * `is_O_with c f g l` : "f is big O of g along l with constant c";
15 * `is_O f g l` : "f is big O of g along l";
16 * `is_o f g l` : "f is little o of g along l".
17
18 Here `l` is any filter on the domain of `f` and `g`, which are assumed to be the same. The codomains
19 of `f` and `g` do not need to be the same; all that is needed that there is a norm associated with
20 these types, and it is the norm that is compared asymptotically.
21
22 The relation `is_O_with c` is introduced to factor out common algebraic arguments in the proofs of
23 similar properties of `is_O` and `is_o`. Usually proofs outside of this file should use `is_O`
24 instead.
25
26 Often the ranges of `f` and `g` will be the real numbers, in which case the norm is the absolute
27 value. In general, we have
28
29 `is_O f g l ↔ is_O (λ x, ∥f x∥) (λ x, ∥g x∥) l`,
30
31 and similarly for `is_o`. But our setup allows us to use the notions e.g. with functions
32 to the integers, rationals, complex numbers, or any normed vector space without mentioning the
33 norm explicitly.
34
35 If `f` and `g` are functions to a normed field like the reals or complex numbers and `g` is always
36 nonzero, we have
37
38 `is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0)`.
39
40 In fact, the right-to-left direction holds without the hypothesis on `g`, and in the other direction
41 it suffices to assume that `f` is zero wherever `g` is. (This generalization is useful in defining
42 the Fréchet derivative.)
43 -/
44
45 open filter set
46 open_locale topological_space
47
48 namespace asymptotics
49
50 variables {α : Type*} {β : Type*} {E : Type*} {F : Type*} {G : Type*}
51 {E' : Type*} {F' : Type*} {G' : Type*} {R : Type*} {R' : Type*} {𝕜 : Type*} {𝕜' : Type*}
52
53 variables [has_norm E] [has_norm F] [has_norm G] [normed_group E'] [normed_group F']
id └──────┘ └──────┘ └──────┘ └──────────┘ └──────────┘
src └──────┘ └──────┘ └──────┘ └──────────┘ └──────────┘
typ └──────┘ └──────┘ └──────┘ └──────────┘ └──────────┘
doc └──────┘ └──────┘ └──────┘ └──────────┘ └──────────┘
54 [normed_group G'] [normed_ring R] [normed_ring R'] [normed_field 𝕜] [normed_field 𝕜']
id └──────────┘ └─────────┘ └─────────┘ └──────────┘ └──────────┘
src └──────────┘ └─────────┘ └─────────┘ └──────────┘ └──────────┘
typ └──────────┘ └─────────┘ └─────────┘ └──────────┘ └──────────┘
doc └──────────┘ └─────────┘ └─────────┘ └──────────┘ └──────────┘
55 {c c' : ℝ} {f : α → E} {g : α → F} {k : α → G} {f' : α → E'} {g' : α → F'} {k' : α → G'}
id ┴
src ┴
typ ┴
56 {l l' : filter α}
id └────┘
src └────┘
typ └────┘
57
58 section defs
59
60 /-! ### Definitions -/
61
62 /-- This version of the Landau notation `is_O_with C f g l` where `f` and `g` are two functions on
63 a type `α` and `l` is a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by `C * ∥g∥`.
64 In other words, `∥f∥ / ∥g∥` is eventually bounded by `C`, modulo division by zero issues that are
65 avoided by this definition. Probably you want to use `is_O` instead of this relation. -/
66 def is_O_with (c : ℝ) (f : α → E) (g : α → F) (l : filter α) : Prop :=
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴
src ┴ └────┘
typ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
67 ∀ᶠ x in l, ∥ f x ∥ ≤ c * ∥ g x ∥
id └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
typ └┘ ┴ └┘ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └┘ └┘ ┴
68
69 /-- The Landau notation `is_O f g l` where `f` and `g` are two functions on a type `α` and `l` is
70 a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by a constant multiple of `∥g∥`.
71 In other words, `∥f∥ / ∥g∥` is eventually bounded, modulo division by zero issues that are avoided
72 by this definition. -/
73 def is_O (f : α → E) (g : α → F) (l : filter α) : Prop := ∃ c : ℝ, is_O_with c f g l
id ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴ └───────┘ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴┴ └───────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
74
75 /-- The Landau notation `is_o f g l` where `f` and `g` are two functions on a type `α` and `l` is
76 a filter on `α`, means that eventually for `l`, `∥f∥` is bounded by an arbitrarily small constant
77 multiple of `∥g∥`. In other words, `∥f∥ / ∥g∥` tends to `0` along `l`, modulo division by zero
78 issues that are avoided by this definition. -/
79 def is_o (f : α → E) (g : α → F) (l : filter α) : Prop := ∀ ⦃c : ℝ⦄, 0 < c → is_O_with c f g l
id ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └────┘ ┴ ┴ └───────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
80
81 end defs
82
83 /-! ### Conversions -/
84
85 theorem is_O_with.is_O (h : is_O_with c f g l) : is_O f g l := ⟨c, h⟩
id └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └──┘
typ └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └──┘
86
87 theorem is_o.is_O_with (hgf : is_o f g l) : is_O_with 1 f g l := hgf zero_lt_one
id └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ └─────────┘
src └──┘ └───────┘ └─────────┘
typ └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─┘ └─────────┘
doc └──┘ └───────┘
88
89 theorem is_o.is_O (hgf : is_o f g l) : is_O f g l := hgf.is_O_with.is_O
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘└────────┘└───┘
src └──┘ └──┘ └────────┘└───┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ └─┘└────────┘└───┘
doc └──┘ └──┘
90
91 theorem is_O_with.weaken (h : is_O_with c f g' l) (hc : c ≤ c') : is_O_with c' f g' l :=
id └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └───────┘ └┘ ┴ └┘ ┴
src └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └───────┘ └┘ ┴ └┘ ┴
doc └───────┘ └───────┘
92 mem_sets_of_superset h $ λ x hx,
id └──────────────────┘ ┴ ┴ └┘
src └──────────────────┘
typ └──────────────────┘ ┴ ┴ └┘
93 calc ∥f x∥ ≤ c * ∥g' x∥ : hx
id ┴┴ ┴┴ ┴ ┴ ┴└┘ ┴┴ └┘
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴┴ ┴ ┴ ┴└┘ ┴┴ └┘
94 ... ≤ _ : mul_le_mul_of_nonneg_right hc (norm_nonneg _)
id └────────────────────────┘ └┘ └─────────┘
src └────────────────────────┘ └─────────┘
typ └────────────────────────┘ └┘ └─────────┘
95
96 theorem is_O_with.exists_pos (h : is_O_with c f g' l) :
id └───────┘ ┴ ┴ └┘ ┴
src └───────┘
typ └───────┘ ┴ ┴ └┘ ┴
doc └───────┘
97 ∃ c' (H : 0 < c'), is_O_with c' f g' l :=
id ┴ └┘ ┴ └┘ ┴ └───────┘ └┘ ┴ └┘ ┴
src ┴ ┴ ┴ └───────┘
typ ┴ └┘ ┴ └┘ ┴ └───────┘ └┘ ┴ └┘ ┴
doc └───────┘
98 ⟨max c 1, lt_of_lt_of_le zero_lt_one (le_max_right c 1), h.weaken $ le_max_left c 1⟩
id └─┘ ┴ └────────────┘ └─────────┘ └──────────┘ ┴ ┴└─────┘ └─────────┘ ┴
src └─┘ └────────────┘ └─────────┘ └──────────┘ └─────┘ └─────────┘
typ └─┘ ┴ └────────────┘ └─────────┘ └──────────┘ ┴ ┴└─────┘ └─────────┘ ┴
99
100 theorem is_O.exists_pos (h : is_O f g' l) : ∃ c (H : 0 < c), is_O_with c f g' l :=
id └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
src └──┘ ┴ ┴ ┴ └───────┘
typ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
doc └──┘ └───────┘
101 let ⟨c, hc⟩ := h in hc.exists_pos
id └─┘ └┘ ┴ └─────────┘
src └─────────┘
typ └─┘ └┘ ┴ └─────────┘
102
103 theorem is_O_with.exists_nonneg (h : is_O_with c f g' l) :
id └───────┘ ┴ ┴ └┘ ┴
src └───────┘
typ └───────┘ ┴ ┴ └┘ ┴
doc └───────┘
104 ∃ c' (H : 0 ≤ c'), is_O_with c' f g' l :=
id ┴ └┘ ┴ └┘ ┴ └───────┘ └┘ ┴ └┘ ┴
src ┴ ┴ ┴ └───────┘
typ ┴ └┘ ┴ └┘ ┴ └───────┘ └┘ ┴ └┘ ┴
doc └───────┘
105 let ⟨c, cpos, hc⟩ := h.exists_pos in ⟨c, le_of_lt cpos, hc⟩
id └─┘ ┴ └──┘ └┘ ┴└─────────┘ └──────┘
src └─────────┘ └──────┘
typ └─┘ ┴ └──┘ └┘ ┴└─────────┘ └──────┘
106
107 theorem is_O.exists_nonneg (h : is_O f g' l) :
id └──┘ ┴ └┘ ┴
src └──┘
typ └──┘ ┴ └┘ ┴
doc └──┘
108 ∃ c (H : 0 ≤ c), is_O_with c f g' l :=
id ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
src ┴ ┴ ┴ └───────┘
typ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
doc └───────┘
109 let ⟨c, hc⟩ := h in hc.exists_nonneg
id └─┘ └┘ ┴ └────────────┘
src └────────────┘
typ └─┘ └┘ ┴ └────────────┘
110
111 /-! ### Congruence -/
112
113 theorem is_O_with_congr {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
114 (hc : c₁ = c₂) (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id └┘ ┴ └┘ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ ┴ └┘ └┘ ┴
115 is_O_with c₁ f₁ g₁ l ↔ is_O_with c₂ f₂ g₂ l :=
id └───────┘ └┘ └┘ └┘ ┴ ┴ └───────┘ └┘ └┘ └┘ ┴
src └───────┘ ┴ └───────┘
typ └───────┘ └┘ └┘ └┘ ┴ ┴ └───────┘ └┘ └┘ └┘ ┴
doc └───────┘ └───────┘
116 begin
st └─────
117 subst c₂,
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────┘└─
118 apply filter.congr_sets,
id └───────────────┘
src └────┘└───────────────┘
typ └────┘└───────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────────────┘└─
119 filter_upwards [hf, hg],
src └──────────────┘ └┘ ┴
typ └──────────────┘ └┘ ┴
doc └──────────────┘ └┘ ┴
txt └──────────────┘ └┘ ┴
par └──────────────┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────┘└─
120 assume x e₁ e₂,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └────────────┘
st ───────────────┘└─
121 dsimp at e₁ e₂ ⊢,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid ┴└────────┘
st ─────────────────┘└─
122 rw [e₁, e₂]
id └┘ └┘
src └──┘ └┘ └┘
typ └──┘└┘└┘└┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───────┘└──┘┴┴
123 end
st └─┘
124
125 theorem is_O_with.congr' {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
126 (hc : c₁ = c₂) (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id └┘ ┴ └┘ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
src ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴
typ └┘ ┴ └┘ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ ┴ └┘ └┘ ┴
127 is_O_with c₁ f₁ g₁ l → is_O_with c₂ f₂ g₂ l :=
id └───────┘ └┘ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
src └───────┘ └───────┘
typ └───────┘ └┘ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
doc └───────┘ └───────┘
128 (is_O_with_congr hc hf hg).mp
id └─────────────┘ └┘ └┘ └┘ └┘
src └─────────────┘ └┘
typ └─────────────┘ └┘ └┘ └┘ └┘
129
130 theorem is_O_with.congr {c₁ c₂} {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
131 (hc : c₁ = c₂) (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
id └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴ ┴
typ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
132 is_O_with c₁ f₁ g₁ l → is_O_with c₂ f₂ g₂ l :=
id └───────┘ └┘ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
src └───────┘ └───────┘
typ └───────┘ └┘ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
doc └───────┘ └───────┘
133 λ h, h.congr' hc (univ_mem_sets' hf) (univ_mem_sets' hg)
id ┴ ┴└─────┘ └┘ └────────────┘ └┘ └────────────┘ └┘
src └─────┘ └────────────┘ └────────────┘
typ ┴ ┴└─────┘ └┘ └────────────┘ └┘ └────────────┘ └┘
134
135 theorem is_O_with.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
id ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
136 is_O_with c f₁ g l → is_O_with c f₂ g l :=
id └───────┘ ┴ └┘ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴
src └───────┘ └───────┘
typ └───────┘ ┴ └┘ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴
doc └───────┘ └───────┘
137 is_O_with.congr rfl hf (λ _, rfl)
id └─────────────┘ └─┘ └┘ ┴ └─┘
src └─────────────┘ └─┘ └─┘
typ └─────────────┘ └─┘ └┘ ┴ └─┘
138
139 theorem is_O_with.congr_right {g₁ g₂ : α → F} {l : filter α} (hg : ∀ x, g₁ x = g₂ x) :
id ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
140 is_O_with c f g₁ l → is_O_with c f g₂ l :=
id └───────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ └┘ ┴
src └───────┘ └───────┘
typ └───────┘ ┴ ┴ └┘ ┴ └───────┘ ┴ ┴ └┘ ┴
doc └───────┘ └───────┘
141 is_O_with.congr rfl (λ _, rfl) hg
id └─────────────┘ └─┘ ┴ └─┘ └┘
src └─────────────┘ └─┘ └─┘
typ └─────────────┘ └─┘ ┴ └─┘ └┘
142
143 theorem is_O_with.congr_const {c₁ c₂} {l : filter α} (hc : c₁ = c₂) :
id └────┘ ┴ └┘ ┴ └┘
src └────┘ ┴
typ └────┘ ┴ └┘ ┴ └┘
144 is_O_with c₁ f g l → is_O_with c₂ f g l :=
id └───────┘ └┘ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴
src └───────┘ └───────┘
typ └───────┘ └┘ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴
doc └───────┘ └───────┘
145 is_O_with.congr hc (λ _, rfl) (λ _, rfl)
id └─────────────┘ └┘ ┴ └─┘ ┴ └─┘
src └─────────────┘ └─┘ └─┘
typ └─────────────┘ └┘ ┴ └─┘ ┴ └─┘
146
147 theorem is_O_congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
148 (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴
typ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ ┴ └┘ └┘ ┴
149 is_O f₁ g₁ l ↔ is_O f₂ g₂ l :=
id └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ └──┘
typ └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
150 exists_congr $ λ c, is_O_with_congr rfl hf hg
id └──────────┘ ┴ └─────────────┘ └─┘ └┘ └┘
src └──────────┘ └─────────────┘ └─┘
typ └──────────┘ ┴ └─────────────┘ └─┘ └┘ └┘
151
152 theorem is_O.congr' {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
153 (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴
typ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ ┴ └┘ └┘ ┴
154 is_O f₁ g₁ l → is_O f₂ g₂ l :=
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
155 (is_O_congr hf hg).mp
id └────────┘ └┘ └┘ └┘
src └────────┘ └┘
typ └────────┘ └┘ └┘ └┘
156
157 theorem is_O.congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
158 (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
id ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
159 is_O f₁ g₁ l → is_O f₂ g₂ l :=
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
160 λ h, h.congr' (univ_mem_sets' hf) (univ_mem_sets' hg)
id ┴ ┴└─────┘ └────────────┘ └┘ └────────────┘ └┘
src └─────┘ └────────────┘ └────────────┘
typ ┴ ┴└─────┘ └────────────┘ └┘ └────────────┘ └┘
161
162 theorem is_O.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
id ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
163 is_O f₁ g l → is_O f₂ g l :=
id └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ └──┘
typ └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘
164 is_O.congr hf (λ _, rfl)
id └────────┘ └┘ ┴ └─┘
src └────────┘ └─┘
typ └────────┘ └┘ ┴ └─┘
165
166 theorem is_O.congr_right {g₁ g₂ : α → E} {l : filter α} (hg : ∀ x, g₁ x = g₂ x) :
id ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
167 is_O f g₁ l → is_O f g₂ l :=
id └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
src └──┘ └──┘
typ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘
168 is_O.congr (λ _, rfl) hg
id └────────┘ ┴ └─┘ └┘
src └────────┘ └─┘
typ └────────┘ ┴ └─┘ └┘
169
170 theorem is_o_congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
171 (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴
typ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ ┴ └┘ └┘ ┴
172 is_o f₁ g₁ l ↔ is_o f₂ g₂ l :=
id └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ └──┘
typ └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
173 ball_congr (λ c hc, is_O_with_congr (eq.refl c) hf hg)
id └────────┘ ┴ └┘ └─────────────┘ └─────┘ ┴ └┘ └┘
src └────────┘ └─────────────┘ └─────┘
typ └────────┘ ┴ └┘ └─────────────┘ └─────┘ ┴ └┘ └┘
174
175 theorem is_o.congr' {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
176 (hf : ∀ᶠ x in l, f₁ x = f₂ x) (hg : ∀ᶠ x in l, g₁ x = g₂ x) :
id └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
src └┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴
typ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴ └┘ ┴
doc └┘ └┘ ┴ └┘ └┘ ┴
177 is_o f₁ g₁ l → is_o f₂ g₂ l :=
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
178 (is_o_congr hf hg).mp
id └────────┘ └┘ └┘ └┘
src └────────┘ └┘
typ └────────┘ └┘ └┘ └┘
179
180 theorem is_o.congr {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : filter α}
id ┴ ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ ┴ └────┘ ┴
181 (hf : ∀ x, f₁ x = f₂ x) (hg : ∀ x, g₁ x = g₂ x) :
id ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src ┴ ┴
typ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
182 is_o f₁ g₁ l → is_o f₂ g₂ l :=
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
183 λ h, h.congr' (univ_mem_sets' hf) (univ_mem_sets' hg)
id ┴ ┴└─────┘ └────────────┘ └┘ └────────────┘ └┘
src └─────┘ └────────────┘ └────────────┘
typ ┴ ┴└─────┘ └────────────┘ └┘ └────────────┘ └┘
184
185 theorem is_o.congr_left {f₁ f₂ : α → E} {l : filter α} (hf : ∀ x, f₁ x = f₂ x) :
id ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
186 is_o f₁ g l → is_o f₂ g l :=
id └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ └──┘
typ └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘
187 is_o.congr hf (λ _, rfl)
id └────────┘ └┘ ┴ └─┘
src └────────┘ └─┘
typ └────────┘ └┘ ┴ └─┘
188
189 theorem is_o.congr_right {g₁ g₂ : α → E} {l : filter α} (hg : ∀ x, g₁ x = g₂ x) :
id ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
src └────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴
190 is_o f g₁ l → is_o f g₂ l :=
id └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
src └──┘ └──┘
typ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘
191 is_o.congr (λ _, rfl) hg
id └────────┘ ┴ └─┘ └┘
src └────────┘ └─┘
typ └────────┘ ┴ └─┘ └┘
192
193 /-! ### Filter operations and transitivity -/
194
195 theorem is_O_with.comp_tendsto (hcfg : is_O_with c f g l)
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
196 {k : β → α} {l' : filter β} (hk : tendsto k l' l):
id ┴ ┴ └────┘ ┴ └─────┘ ┴ └┘ ┴
src └────┘ └─────┘
typ ┴ ┴ └────┘ ┴ └─────┘ ┴ └┘ ┴
doc └─────┘
197 is_O_with c (f ∘ k) (g ∘ k) l' :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └───────┘
198 hk hcfg
id └┘ └──┘
typ └┘ └──┘
199
200 theorem is_O.comp_tendsto (hfg : is_O f g l) {k : β → α} {l' : filter β} (hk : tendsto k l' l) :
id └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─────┘ ┴ └┘ ┴
src └──┘ └────┘ └─────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─────┘ ┴ └┘ ┴
doc └──┘ └─────┘
201 is_O (f ∘ k) (g ∘ k) l' :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └──┘
202 hfg.imp (λ c h, h.comp_tendsto hk)
id └─┘└──┘ ┴ ┴ ┴└───────────┘ └┘
src └──┘ └───────────┘
typ └─┘└──┘ ┴ ┴ ┴└───────────┘ └┘
203
204 theorem is_o.comp_tendsto (hfg : is_o f g l) {k : β → α} {l' : filter β} (hk : tendsto k l' l) :
id └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─────┘ ┴ └┘ ┴
src └──┘ └────┘ └─────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ └─────┘ ┴ └┘ ┴
doc └──┘ └─────┘
205 is_o (f ∘ k) (g ∘ k) l' :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘
doc └──┘
206 λ c cpos, (hfg cpos).comp_tendsto hk
id ┴ └──┘ └─┘ └──┘ └──────────┘ └┘
src └──────────┘
typ ┴ └──┘ └─┘ └──┘ └──────────┘ └┘
207
208 theorem is_O_with.mono (h : is_O_with c f g l') (hl : l ≤ l') : is_O_with c f g l :=
id └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ └┘ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘
209 hl h
id └┘ ┴
typ └┘ ┴
210
211 theorem is_O.mono (h : is_O f g l') (hl : l ≤ l') : is_O f g l :=
id └──┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
212 h.imp (λ c h, h.mono hl)
id ┴└──┘ ┴ ┴ ┴└───┘ └┘
src └──┘ └───┘
typ ┴└──┘ ┴ ┴ ┴└───┘ └┘
213
214 theorem is_o.mono (h : is_o f g l') (hl : l ≤ l') : is_o f g l :=
id └──┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ └┘ ┴ ┴ └┘ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
215 λ c cpos, (h cpos).mono hl
id ┴ └──┘ ┴ └──┘ └──┘ └┘
src └──┘
typ ┴ └──┘ ┴ └──┘ └──┘ └┘
216
217 theorem is_O_with.trans (hfg : is_O_with c f g l) (hgk : is_O_with c' g k l) (hc : 0 ≤ c) :
id └───────┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ └───────┘ └┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘
218 is_O_with (c * c') f k l :=
id └───────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
219 begin
st └─────
220 filter_upwards [hfg, hgk],
src └──────────────┘ └┘ ┴
typ └──────────────┘ └┘ ┴
doc └──────────────┘ └┘ ┴
txt └──────────────┘ └┘ ┴
par └──────────────┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────────┘└─
221 assume x hx hx',
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └─────────────┘
st ────────────────┘└─
222 calc ∥f x∥ ≤ c * ∥g x∥ : hx
id └──┘ ┴┴ ┴ ┴ ┴ ┴ └┘
src └──┘ ┴ ┴
typ └──┘ ┴┴ ┴ ┴ ┴ ┴ └┘
doc └──┘
st ──────────────────────────────
223 ... ≤ c * (c' * ∥k x∥) : mul_le_mul_of_nonneg_left hx' hc
id ┴ └───────────────────────┘ └─┘ └┘
src ┴ └───────────────────────┘
typ ┴ └───────────────────────┘ └─┘ └┘
st ────────────────────────────────────────────────────────────
224 ... = c * c' * ∥k x∥ : (mul_assoc _ _ _).symm
id └┘ ┴ └───────┘ └──┘
src └───────┘ └──┘
typ └┘ ┴ └───────┘ └──┘
st ─────────────────────────────────────────────┘└─
225 end
st ──┘
226
227 theorem is_O.trans (hfg : is_O f g' l) (hgk : is_O g' k l) : is_O f k l :=
id └──┘ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
228 let ⟨c, cnonneg, hc⟩ := hfg.exists_nonneg, ⟨c', hc'⟩ := hgk in (hc.trans hc' cnonneg).is_O
id └─┘ └─────┘ └┘ └─┘└────────────┘ └─┘ └─┘ └────┘ └──┘
src └────────────┘ └────┘ └──┘
typ └─┘ └─────┘ └┘ └─┘└────────────┘ └─┘ └─┘ └────┘ └──┘
229
230 theorem is_o.trans_is_O_with (hfg : is_o f g l) (hgk : is_O_with c g k l) (hc : 0 < c) :
id └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ └───────┘ ┴
typ └──┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └───────┘
231 is_o f k l :=
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
doc └──┘
232 begin
st └─────
233 intros c' c'pos,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
234 have : 0 < c' / c, from div_pos c'pos hc,
id ┴ └┘ ┴ ┴ └─────┘ └───┘ └┘
src └───────┘┴┴ ┴┴┴ └───┘└─────┘┴ ┴
typ └───────┘┴┴└┘┴┴┴┴ └───┘└─────┘┴└───┘┴└┘
doc └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
txt └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
par └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
pid └───┘└──┘ ┴ ┴ ┴ └───┘ ┴ ┴
st ──────────────────┘└─────────────────────┘└─
235 exact ((hfg this).trans hgk (le_of_lt this)).congr_const (div_mul_cancel _ (ne_of_gt hc))
id └─┘ └─┘ └──────┘ └──┘ └────────────┘ └──────┘ └┘
src └────┘ ┴ └──────┘ ┴ └──────┘┴ └─────────────┘ └────────────┘└─┘ └──────┘┴ └─┘
typ └────┘ └─┘┴ └──────┘└─┘┴ └──────┘┴└──┘└─────────────┘ └────────────┘└─┘ └──────┘┴└┘└─┘
doc └────┘ ┴ └──────┘ ┴ ┴ └─────────────┘ └─┘ ┴ └─┘
txt └────┘ ┴ └──────┘ ┴ ┴ └─────────────┘ └─┘ ┴ └─┘
par └────┘ ┴ └──────┘ ┴ ┴ └─────────────┘ └─┘ ┴ └─┘
pid ┴ ┴ └──────┘ ┴ ┴ └─────────────┘ └─┘ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘
236 end
st └─┘
237
238 theorem is_o.trans_is_O (hfg : is_o f g l) (hgk : is_O g k' l) : is_o f k' l :=
id └──┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
239 let ⟨c, cpos, hc⟩ := hgk.exists_pos in hfg.trans_is_O_with hc cpos
id └─┘ └──┘ └┘ └─┘└─────────┘ └─┘└──────────────┘
src └─────────┘ └──────────────┘
typ └─┘ └──┘ └┘ └─┘└─────────┘ └─┘└──────────────┘
240
241 theorem is_O_with.trans_is_o (hfg : is_O_with c f g l) (hgk : is_o g k l) (hc : 0 < c) :
id └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └──┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘ └──┘
242 is_o f k l :=
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
doc └──┘
243 begin
st └─────
244 intros c' c'pos,
src └─────────────┘
typ └─────────────┘
doc └─────────────┘
txt └─────────────┘
par └─────────────┘
pid └───────┘
st ────────────────┘└─
245 have : 0 < c' / c, from div_pos c'pos hc,
id ┴ └┘ ┴ ┴ └─────┘ └───┘ └┘
src └───────┘┴┴ ┴┴┴ └───┘└─────┘┴ ┴
typ └───────┘┴┴└┘┴┴┴┴ └───┘└─────┘┴└───┘┴└┘
doc └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
txt └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
par └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
pid └───┘└──┘ ┴ ┴ ┴ └───┘ ┴ ┴
st ──────────────────┘└─────────────────────┘└─
246 exact (hfg.trans (hgk this) (le_of_lt hc)).congr_const (mul_div_cancel' _ (ne_of_gt hc))
id └───────┘ └─┘ └──┘ └──────┘ └─────────────┘ └──────┘ └┘
src └────┘ └───────┘┴ ┴ └┘ └──────┘┴ └─────────────┘ └─────────────┘└─┘ └──────┘┴ └─┘
typ └────┘ └───────┘┴ └─┘┴└──┘└┘ └──────┘┴ └─────────────┘ └─────────────┘└─┘ └──────┘┴└┘└─┘
doc └────┘ ┴ ┴ └┘ ┴ └─────────────┘ └─┘ ┴ └─┘
txt └────┘ ┴ ┴ └┘ ┴ └─────────────┘ └─┘ ┴ └─┘
par └────┘ ┴ ┴ └┘ ┴ └─────────────┘ └─┘ ┴ └─┘
pid ┴ ┴ ┴ └┘ ┴ └─────────────┘ └─┘ ┴ └┘┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘
247 end
st └─┘
248
249 theorem is_O.trans_is_o (hfg : is_O f g' l) (hgk : is_o g' k l) : is_o f k l :=
id └──┘ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
250 let ⟨c, cpos, hc⟩ := hfg.exists_pos in hc.trans_is_o hgk cpos
id └─┘ └──┘ └┘ └─┘└─────────┘ └─────────┘ └─┘
src └─────────┘ └─────────┘
typ └─┘ └──┘ └┘ └─┘└─────────┘ └─────────┘ └─┘
251
252 theorem is_o.trans (hfg : is_o f g l) (hgk : is_o g k' l) : is_o f k' l :=
id └──┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
253 hfg.trans_is_O hgk.is_O
id └─┘└─────────┘ └─┘└───┘
src └─────────┘ └───┘
typ └─┘└─────────┘ └─┘└───┘
254
255 theorem is_o.trans' (hfg : is_o f g' l) (hgk : is_o g' k l) : is_o f k l :=
id └──┘ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘
typ └──┘ ┴ └┘ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
256 hfg.is_O.trans_is_o hgk
id └─┘└───┘└─────────┘ └─┘
src └───┘└─────────┘
typ └─┘└───┘└─────────┘ └─┘
257
258 section
259
260 variable (l)
261
262 theorem is_O_with_of_le' (hfg : ∀ x, ∥f x∥ ≤ c * ∥g x∥) : is_O_with c f g l :=
id ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └───────┘ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └───────┘
typ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
263 univ_mem_sets' hfg
id └────────────┘ └─┘
src └────────────┘
typ └────────────┘ └─┘
264
265 theorem is_O_with_of_le (hfg : ∀ x, ∥f x∥ ≤ ∥g x∥) : is_O_with 1 f g l :=
id ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └───────┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └───────┘
typ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └───────┘ ┴ ┴ ┴
doc └───────┘
266 is_O_with_of_le' l $ λ x, by { rw one_mul, exact hfg x }
id └──────────────┘ ┴ ┴ └─────┘ └─┘ ┴
src └──────────────┘ └─┘└─────┘ └────┘ ┴ ┴
typ └──────────────┘ ┴ ┴ └─┘└─────┘ └────┘└─┘┴┴┴
doc └─┘ └────┘ ┴ ┴
txt └─┘ └────┘ ┴ ┴
par └─┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st └───────────┘└────────────┘└┘
267
268 theorem is_O_of_le' (hfg : ∀ x, ∥f x∥ ≤ c * ∥g x∥) : is_O f g l :=
id ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴┴ ┴┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴
doc └──┘
269 (is_O_with_of_le' l hfg).is_O
id └──────────────┘ ┴ └─┘ └──┘
src └──────────────┘ └──┘
typ └──────────────┘ ┴ └─┘ └──┘
270
271 theorem is_O_of_le (hfg : ∀ x, ∥f x∥ ≤ ∥g x∥) : is_O f g l :=
id ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴
src ┴ ┴ ┴ ┴ ┴ └──┘
typ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴
doc └──┘
272 (is_O_with_of_le l hfg).is_O
id └─────────────┘ ┴ └─┘ └──┘
src └─────────────┘ └──┘
typ └─────────────┘ ┴ └─┘ └──┘
273
274 end
275
276 theorem is_O_with_refl (f : α → E) (l : filter α) : is_O_with 1 f f l :=
id ┴ ┴ └────┘ ┴ └───────┘ ┴ ┴ ┴
src └────┘ └───────┘
typ ┴ ┴ └────┘ ┴ └───────┘ ┴ ┴ ┴
doc └───────┘
277 is_O_with_of_le l $ λ _, le_refl _
id └─────────────┘ ┴ ┴ └─────┘
src └─────────────┘ └─────┘
typ └─────────────┘ ┴ ┴ └─────┘
278
279 theorem is_O_refl (f : α → E) (l : filter α) : is_O f f l := (is_O_with_refl f l).is_O
id ┴ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └──┘
src └────┘ └──┘ └────────────┘ └──┘
typ ┴ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └──┘
doc └──┘
280
281 theorem is_O_with.trans_le (hfg : is_O_with c f g l) (hgk : ∀ x, ∥g x∥ ≤ ∥k x∥) (hc : 0 ≤ c) :
id └───────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ ┴ ┴┴ ┴┴ ┴ ┴
doc └───────┘
282 is_O_with c f k l :=
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘
283 (hfg.trans (is_O_with_of_le l hgk) hc).congr_const $ mul_one c
id └─┘└────┘ └─────────────┘ ┴ └─┘ └┘ └─────────┘ └─────┘ ┴
src └────┘ └─────────────┘ └─────────┘ └─────┘
typ └─┘└────┘ └─────────────┘ ┴ └─┘ └┘ └─────────┘ └─────┘ ┴
284
285 theorem is_O.trans_le (hfg : is_O f g' l) (hgk : ∀ x, ∥g' x∥ ≤ ∥k x∥) :
id └──┘ ┴ └┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴┴ ┴┴
src └──┘ ┴ ┴ ┴ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴┴ ┴┴
doc └──┘
286 is_O f k l :=
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
doc └──┘
287 hfg.trans (is_O_of_le l hgk)
id └─┘└────┘ └────────┘ ┴ └─┘
src └────┘ └────────┘
typ └─┘└────┘ └────────┘ ┴ └─┘
288
289 section bot
290
291 variables (c f g)
292
293 theorem is_O_with_bot : is_O_with c f g ⊥ := trivial
id └───────┘ ┴ ┴ ┴ ┴ └─────┘
src └───────┘ ┴ └─────┘
typ └───────┘ ┴ ┴ ┴ ┴ └─────┘
doc └───────┘
294
295 theorem is_O_bot : is_O f g ⊥ := (is_O_with_bot c f g).is_O
id └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──┘
src └──┘ ┴ └───────────┘ └──┘
typ └──┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴ └──┘
doc └──┘
296
297 theorem is_o_bot : is_o f g ⊥ := λ c _, is_O_with_bot c f g
id └──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
src └──┘ ┴ └───────────┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴ ┴ ┴
doc └──┘
298
299 end bot
300
301 theorem is_O_with.join (h : is_O_with c f g l) (h' : is_O_with c f g l') :
id └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘
src └───────┘ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └┘
doc └───────┘ └───────┘
302 is_O_with c f g (l ⊔ l') :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ └┘
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ └┘
doc └───────┘
303 mem_sup_sets.2 ⟨h, h'⟩
id └──────────┘┴ ┴ └┘
src └──────────┘┴
typ └──────────┘┴ ┴ └┘
304
305 theorem is_O_with.join' (h : is_O_with c f g' l) (h' : is_O_with c' f g' l') :
id └───────┘ ┴ ┴ └┘ ┴ └───────┘ └┘ ┴ └┘ └┘
src └───────┘ └───────┘
typ └───────┘ ┴ ┴ └┘ ┴ └───────┘ └┘ ┴ └┘ └┘
doc └───────┘ └───────┘
306 is_O_with (max c c') f g' (l ⊔ l') :=
id └───────┘ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘
src └───────┘ └─┘ ┴
typ └───────┘ └─┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘
doc └───────┘
307 mem_sup_sets.2 ⟨(h.weaken $ le_max_left c c'), (h'.weaken $ le_max_right c c')⟩
id └──────────┘┴ ┴└─────┘ └─────────┘ ┴ └┘ └┘└─────┘ └──────────┘ ┴ └┘
src └──────────┘┴ └─────┘ └─────────┘ └─────┘ └──────────┘
typ └──────────┘┴ ┴└─────┘ └─────────┘ ┴ └┘ └┘└─────┘ └──────────┘ ┴ └┘
308
309 theorem is_O.join (h : is_O f g' l) (h' : is_O f g' l') : is_O f g' (l ⊔ l') :=
id └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ └┘ └──┘ ┴ └┘ ┴ ┴ └┘
src └──┘ └──┘ └──┘ ┴
typ └──┘ ┴ └┘ ┴ └──┘ ┴ └┘ └┘ └──┘ ┴ └┘ ┴ ┴ └┘
doc └──┘ └──┘ └──┘
310 let ⟨c, hc⟩ := h, ⟨c', hc'⟩ := h' in (hc.join' hc').is_O
id └─┘ └┘ ┴ └─┘ └┘ └────┘ └──┘
src └────┘ └──┘
typ └─┘ └┘ ┴ └─┘ └┘ └────┘ └──┘
311
312 theorem is_o.join (h : is_o f g l) (h' : is_o f g l') :
id └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘
src └──┘ └──┘
typ └──┘ ┴ ┴ ┴ └──┘ ┴ ┴ └┘
doc └──┘ └──┘
313 is_o f g (l ⊔ l') :=
id └──┘ ┴ ┴ ┴ ┴ └┘
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ └┘
doc └──┘
314 λ c cpos, (h cpos).join (h' cpos)
id ┴ └──┘ ┴ └──┘ └──┘ └┘ └──┘
src └──┘
typ ┴ └──┘ ┴ └──┘ └──┘ └┘ └──┘
315
316 /-! ### Simplification : norm -/
317
318 @[simp] theorem is_O_with_norm_right : is_O_with c f (λ x, ∥g' x∥) l ↔ is_O_with c f g' l :=
id └───────┘ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
src └───────┘ ┴ ┴ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
doc └──┘ └───────┘ └───────┘
319 by simp only [is_O_with, norm_norm]
id └───────┘ └───────┘
src └─────────┘└───────┘└┘└───────┘└─
typ └─────────┘└───────┘└┘└───────┘└─
doc └─────────┘└───────┘└┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └─────────────────────────────────
320
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
321 alias is_O_with_norm_right ↔ asymptotics.is_O_with.of_norm_right asymptotics.is_O_with.norm_right
322
323 @[simp] theorem is_O_norm_right : is_O f (λ x, ∥g' x∥) l ↔ is_O f g' l :=
id └──┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ ┴ └┘ ┴
src └──┘ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
324 exists_congr $ λ _, is_O_with_norm_right
id └──────────┘ ┴ └──────────────────┘
src └──────────┘ └──────────────────┘
typ └──────────┘ ┴ └──────────────────┘
325
326 alias is_O_norm_right ↔ asymptotics.is_O.of_norm_right asymptotics.is_O.norm_right
327
328 @[simp] theorem is_o_norm_right : is_o f (λ x, ∥g' x∥) l ↔ is_o f g' l :=
id └──┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ ┴ └┘ ┴
src └──┘ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
329 forall_congr $ λ _, forall_congr $ λ _, is_O_with_norm_right
id └──────────┘ ┴ └──────────┘ ┴ └──────────────────┘
src └──────────┘ └──────────┘ └──────────────────┘
typ └──────────┘ ┴ └──────────┘ ┴ └──────────────────┘
330
331 alias is_o_norm_right ↔ asymptotics.is_o.of_norm_right asymptotics.is_o.norm_right
332
333 @[simp] theorem is_O_with_norm_left : is_O_with c (λ x, ∥f' x∥) g l ↔ is_O_with c f' g l :=
id └───────┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴
src └───────┘ ┴ ┴ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴
doc └──┘ └───────┘ └───────┘
334 by simp only [is_O_with, norm_norm]
id └───────┘ └───────┘
src └─────────┘└───────┘└┘└───────┘└─
typ └─────────┘└───────┘└┘└───────┘└─
doc └─────────┘└───────┘└┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └─────────────────────────────────
335
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
336 alias is_O_with_norm_left ↔ asymptotics.is_O_with.of_norm_left asymptotics.is_O_with.norm_left
337
338 @[simp] theorem is_O_norm_left : is_O (λ x, ∥f' x∥) g l ↔ is_O f' g l :=
id └──┘ ┴ ┴└┘ ┴┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘ └──┘
339 exists_congr $ λ _, is_O_with_norm_left
id └──────────┘ ┴ └─────────────────┘
src └──────────┘ └─────────────────┘
typ └──────────┘ ┴ └─────────────────┘
340
341 alias is_O_norm_left ↔ asymptotics.is_O.of_norm_left asymptotics.is_O.norm_left
342
343 @[simp] theorem is_o_norm_left : is_o (λ x, ∥f' x∥) g l ↔ is_o f' g l :=
id └──┘ ┴ ┴└┘ ┴┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘ └──┘
344 forall_congr $ λ _, forall_congr $ λ _, is_O_with_norm_left
id └──────────┘ ┴ └──────────┘ ┴ └─────────────────┘
src └──────────┘ └──────────┘ └─────────────────┘
typ └──────────┘ ┴ └──────────┘ ┴ └─────────────────┘
345
346 alias is_o_norm_left ↔ asymptotics.is_o.of_norm_left asymptotics.is_o.norm_left
347
348 theorem is_O_with_norm_norm :
349 is_O_with c (λ x, ∥f' x∥) (λ x, ∥g' x∥) l ↔ is_O_with c f' g' l :=
id └───────┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴└┘ ┴┴ ┴ ┴ └───────┘ ┴ └┘ └┘ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴└┘ ┴┴ ┴ ┴└┘ ┴┴ ┴ ┴ └───────┘ ┴ └┘ └┘ ┴
doc └───────┘ └───────┘
350 is_O_with_norm_left.trans is_O_with_norm_right
id └─────────────────┘└────┘ └──────────────────┘
src └─────────────────┘└────┘ └──────────────────┘
typ └─────────────────┘└────┘ └──────────────────┘
351
352 alias is_O_with_norm_norm ↔ asymptotics.is_O_with.of_norm_norm asymptotics.is_O_with.norm_norm
353
354 theorem is_O_norm_norm :
355 is_O (λ x, ∥f' x∥) (λ x, ∥g' x∥) l ↔ is_O f' g' l :=
id └──┘ ┴ ┴└┘ ┴┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
356 is_O_norm_left.trans is_O_norm_right
id └────────────┘└────┘ └─────────────┘
src └────────────┘└────┘ └─────────────┘
typ └────────────┘└────┘ └─────────────┘
357
358 alias is_O_norm_norm ↔ asymptotics.is_O.of_norm_norm asymptotics.is_O.norm_norm
359
360 theorem is_o_norm_norm :
361 is_o (λ x, ∥f' x∥) (λ x, ∥g' x∥) l ↔ is_o f' g' l :=
id └──┘ ┴ ┴└┘ ┴┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ ┴ ┴ ┴ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴┴ ┴ ┴└┘ ┴┴ ┴ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
362 is_o_norm_left.trans is_o_norm_right
id └────────────┘└────┘ └─────────────┘
src └────────────┘└────┘ └─────────────┘
typ └────────────┘└────┘ └─────────────┘
363
364 alias is_o_norm_norm ↔ asymptotics.is_o.of_norm_norm asymptotics.is_o.norm_norm
365
366 /-! ### Simplification: negate -/
367
368 @[simp] theorem is_O_with_neg_right : is_O_with c f (λ x, -(g' x)) l ↔ is_O_with c f g' l :=
id └───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
src └───────┘ ┴ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴
doc └──┘ └───────┘ └───────┘
369 by simp only [is_O_with, norm_neg]
id └───────┘ └──────┘
src └─────────┘└───────┘└┘└──────┘└─
typ └─────────┘└───────┘└┘└──────┘└─
doc └─────────┘└───────┘└┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────
370
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
371 alias is_O_with_neg_right ↔ asymptotics.is_O_with.of_neg_right asymptotics.is_O_with.neg_right
372
373 @[simp] theorem is_O_neg_right : is_O f (λ x, -(g' x)) l ↔ is_O f g' l :=
id └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
374 exists_congr $ λ _, is_O_with_neg_right
id └──────────┘ ┴ └─────────────────┘
src └──────────┘ └─────────────────┘
typ └──────────┘ ┴ └─────────────────┘
375
376 alias is_O_neg_right ↔ asymptotics.is_O.of_neg_right asymptotics.is_O.neg_right
377
378 @[simp] theorem is_o_neg_right : is_o f (λ x, -(g' x)) l ↔ is_o f g' l :=
id └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
379 forall_congr $ λ _, forall_congr $ λ _, is_O_with_neg_right
id └──────────┘ ┴ └──────────┘ ┴ └─────────────────┘
src └──────────┘ └──────────┘ └─────────────────┘
typ └──────────┘ ┴ └──────────┘ ┴ └─────────────────┘
380
381 alias is_o_neg_right ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_right
382
383 @[simp] theorem is_O_with_neg_left : is_O_with c (λ x, -(f' x)) g l ↔ is_O_with c f' g l :=
id └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴
src └───────┘ ┴ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────┘ ┴ └┘ ┴ ┴
doc └──┘ └───────┘ └───────┘
384 by simp only [is_O_with, norm_neg]
id └───────┘ └──────┘
src └─────────┘└───────┘└┘└──────┘└─
typ └─────────┘└───────┘└┘└──────┘└─
doc └─────────┘└───────┘└┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────
385
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
386 alias is_O_with_neg_left ↔ asymptotics.is_O_with.of_neg_left asymptotics.is_O_with.neg_left
387
388 @[simp] theorem is_O_neg_left : is_O (λ x, -(f' x)) g l ↔ is_O f' g l :=
id └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘ └──┘
389 exists_congr $ λ _, is_O_with_neg_left
id └──────────┘ ┴ └────────────────┘
src └──────────┘ └────────────────┘
typ └──────────┘ ┴ └────────────────┘
390
391 alias is_O_neg_left ↔ asymptotics.is_O.of_neg_left asymptotics.is_O.neg_left
392
393 @[simp] theorem is_o_neg_left : is_o (λ x, -(f' x)) g l ↔ is_o f' g l :=
id └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘ └──┘
394 forall_congr $ λ _, forall_congr $ λ _, is_O_with_neg_left
id └──────────┘ ┴ └──────────┘ ┴ └────────────────┘
src └──────────┘ └──────────┘ └────────────────┘
typ └──────────┘ ┴ └──────────┘ ┴ └────────────────┘
395
396 alias is_o_neg_left ↔ asymptotics.is_o.of_neg_right asymptotics.is_o.neg_left
397
398 /-! ### Product of functions (right) -/
399
400 lemma is_O_with_fst_prod : is_O_with 1 f' (λ x, (f' x, g' x)) l :=
id └───────┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └───────┘
401 is_O_with_of_le l $ λ x, le_max_left _ _
id └─────────────┘ ┴ ┴ └─────────┘
src └─────────────┘ └─────────┘
typ └─────────────┘ ┴ ┴ └─────────┘
402
403 lemma is_O_with_snd_prod : is_O_with 1 g' (λ x, (f' x, g' x)) l :=
id └───────┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └───────┘
404 is_O_with_of_le l $ λ x, le_max_right _ _
id └─────────────┘ ┴ ┴ └──────────┘
src └─────────────┘ └──────────┘
typ └─────────────┘ ┴ ┴ └──────────┘
405
406 lemma is_O_fst_prod : is_O f' (λ x, (f' x, g' x)) l := is_O_with_fst_prod.is_O
id └──┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴ └────────────────┘└───┘
src └──┘ ┴ └────────────────┘└───┘
typ └──┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴ └────────────────┘└───┘
doc └──┘
407
408 lemma is_O_snd_prod : is_O g' (λ x, (f' x, g' x)) l := is_O_with_snd_prod.is_O
id └──┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴ └────────────────┘└───┘
src └──┘ ┴ └────────────────┘└───┘
typ └──┘ └┘ ┴ ┴└┘ ┴ └┘ ┴ ┴ └────────────────┘└───┘
doc └──┘
409
410 section
411
412 variables (f' k')
413
414 lemma is_O_with.prod_rightl (h : is_O_with c f g' l) (hc : 0 ≤ c) :
id └───────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
415 is_O_with c f (λ x, (g' x, k' x)) l :=
id └───────┘ ┴ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └───────┘
416 (h.trans is_O_with_fst_prod hc).congr_const (mul_one c)
id ┴└────┘ └────────────────┘ └┘ └─────────┘ └─────┘ ┴
src └────┘ └────────────────┘ └─────────┘ └─────┘
typ ┴└────┘ └────────────────┘ └┘ └─────────┘ └─────┘ ┴
417
418 lemma is_O.prod_rightl (h : is_O f g' l) : is_O f (λx, (g' x, k' x)) l :=
id └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └──┘ └──┘ ┴
typ └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └──┘ └──┘
419 let ⟨c, cnonneg, hc⟩ := h.exists_nonneg in (hc.prod_rightl k' cnonneg).is_O
id └─┘ └─────┘ └┘ ┴└────────────┘ └──────────┘ └┘ └──┘
src └────────────┘ └──────────┘ └──┘
typ └─┘ └─────┘ └┘ ┴└────────────┘ └──────────┘ └┘ └──┘
420
421 lemma is_o.prod_rightl (h : is_o f g' l) : is_o f (λ x, (g' x, k' x)) l :=
id └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └──┘ └──┘ ┴
typ └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └──┘ └──┘
422 λ c cpos, (h cpos).prod_rightl k' (le_of_lt cpos)
id ┴ └──┘ ┴ └──┘ └─────────┘ └┘ └──────┘ └──┘
src └─────────┘ └──────┘
typ ┴ └──┘ ┴ └──┘ └─────────┘ └┘ └──────┘ └──┘
423
424 lemma is_O_with.prod_rightr (h : is_O_with c f g' l) (hc : 0 ≤ c) :
id └───────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
425 is_O_with c f (λ x, (f' x, g' x)) l :=
id └───────┘ ┴ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └───────┘
426 (h.trans is_O_with_snd_prod hc).congr_const (mul_one c)
id ┴└────┘ └────────────────┘ └┘ └─────────┘ └─────┘ ┴
src └────┘ └────────────────┘ └─────────┘ └─────┘
typ ┴└────┘ └────────────────┘ └┘ └─────────┘ └─────┘ ┴
427
428 lemma is_O.prod_rightr (h : is_O f g' l) : is_O f (λx, (f' x, g' x)) l :=
id └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └──┘ └──┘ ┴
typ └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └──┘ └──┘
429 let ⟨c, cnonneg, hc⟩ := h.exists_nonneg in (hc.prod_rightr f' cnonneg).is_O
id └─┘ └─────┘ └┘ ┴└────────────┘ └──────────┘ └┘ └──┘
src └────────────┘ └──────────┘ └──┘
typ └─┘ └─────┘ └┘ ┴└────────────┘ └──────────┘ └┘ └──┘
430
431 lemma is_o.prod_rightr (h : is_o f g' l) : is_o f (λx, (f' x, g' x)) l :=
id └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
src └──┘ └──┘ ┴
typ └──┘ ┴ └┘ ┴ └──┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ ┴
doc └──┘ └──┘
432 λ c cpos, (h cpos).prod_rightr f' (le_of_lt cpos)
id ┴ └──┘ ┴ └──┘ └─────────┘ └┘ └──────┘ └──┘
src └─────────┘ └──────┘
typ ┴ └──┘ ┴ └──┘ └─────────┘ └┘ └──────┘ └──┘
433
434 end
435
436 lemma is_O_with.prod_left_same (hf : is_O_with c f' k' l) (hg : is_O_with c g' k' l) :
id └───────┘ ┴ └┘ └┘ ┴ └───────┘ ┴ └┘ └┘ ┴
src └───────┘ └───────┘
typ └───────┘ ┴ └┘ └┘ ┴ └───────┘ ┴ └┘ └┘ ┴
doc └───────┘ └───────┘
437 is_O_with c (λ x, (f' x, g' x)) k' l :=
id └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
doc └───────┘
438 begin
st └─────
439 filter_upwards [hf, hg],
src └──────────────┘ └┘ ┴
typ └──────────────┘ └┘ ┴
doc └──────────────┘ └┘ ┴
txt └──────────────┘ └┘ ┴
par └──────────────┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────────┘└─
440 simp only [mem_set_of_eq],
id └───────────┘
src └─────────┘└───────────┘┴
typ └─────────┘└───────────┘┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────────┘└─
441 exact λ x, max_le
id └────┘
src └────┘ └──┘└────┘┴
typ └────┘ └──┘└────┘┴
doc └────┘ └──┘ ┴
txt └────┘ └──┘ ┴
par └────┘ └──┘ ┴
pid ┴ └──┘ ┴
st ───────────────────┘
442 end
st └─┘
443
444 lemma is_O_with.prod_left (hf : is_O_with c f' k' l) (hg : is_O_with c' g' k' l) :
id └───────┘ ┴ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
src └───────┘ └───────┘
typ └───────┘ ┴ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
doc └───────┘ └───────┘
445 is_O_with (max c c') (λ x, (f' x, g' x)) k' l :=
id └───────┘ └─┘ ┴ └┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
src └───────┘ └─┘ ┴
typ └───────┘ └─┘ ┴ └┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
doc └───────┘
446 (hf.weaken $ le_max_left c c').prod_left_same (hg.weaken $ le_max_right c c')
id └┘└─────┘ └─────────┘ ┴ └┘ └────────────┘ └┘└─────┘ └──────────┘ ┴ └┘
src └─────┘ └─────────┘ └────────────┘ └─────┘ └──────────┘
typ └┘└─────┘ └─────────┘ ┴ └┘ └────────────┘ └┘└─────┘ └──────────┘ ┴ └┘
447
448 lemma is_O_with.prod_left_fst (h : is_O_with c (λ x, (f' x, g' x)) k' l) :
id └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
doc └───────┘
449 is_O_with c f' k' l :=
id └───────┘ ┴ └┘ └┘ ┴
src └───────┘
typ └───────┘ ┴ └┘ └┘ ┴
doc └───────┘
450 (is_O_with_fst_prod.trans h zero_le_one).congr_const $ one_mul c
id └────────────────┘└────┘ ┴ └─────────┘ └─────────┘ └─────┘ ┴
src └────────────────┘└────┘ └─────────┘ └─────────┘ └─────┘
typ └────────────────┘└────┘ ┴ └─────────┘ └─────────┘ └─────┘ ┴
451
452 lemma is_O_with.prod_left_snd (h : is_O_with c (λ x, (f' x, g' x)) k' l) :
id └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
doc └───────┘
453 is_O_with c g' k' l :=
id └───────┘ ┴ └┘ └┘ ┴
src └───────┘
typ └───────┘ ┴ └┘ └┘ ┴
doc └───────┘
454 (is_O_with_snd_prod.trans h zero_le_one).congr_const $ one_mul c
id └────────────────┘└────┘ ┴ └─────────┘ └─────────┘ └─────┘ ┴
src └────────────────┘└────┘ └─────────┘ └─────────┘ └─────┘
typ └────────────────┘└────┘ ┴ └─────────┘ └─────────┘ └─────┘ ┴
455
456 lemma is_O_with_prod_left :
457 is_O_with c (λ x, (f' x, g' x)) k' l ↔ is_O_with c f' k' l ∧ is_O_with c g' k' l :=
id └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ ┴ └───────┘ ┴ └┘ └┘ ┴ ┴ └───────┘ ┴ └┘ └┘ ┴
src └───────┘ ┴ ┴ └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ ┴ └───────┘ ┴ └┘ └┘ ┴ ┴ └───────┘ ┴ └┘ └┘ ┴
doc └───────┘ └───────┘ └───────┘
458 ⟨λ h, ⟨h.prod_left_fst, h.prod_left_snd⟩, λ h, h.1.prod_left_same h.2⟩
id ┴ ┴└────────────┘ ┴└────────────┘ ┴ ┴┴ └────────────┘ ┴┴
src └────────────┘ └────────────┘ ┴ └────────────┘ ┴
typ ┴ ┴└────────────┘ ┴└────────────┘ ┴ ┴┴ └────────────┘ ┴┴
459
460 lemma is_O.prod_left (hf : is_O f' k' l) (hg : is_O g' k' l) : is_O (λ x, (f' x, g' x)) k' l :=
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
461 let ⟨c, hf⟩ := hf, ⟨c', hg⟩ := hg in (hf.prod_left hg).is_O
id └─┘ └┘ └┘ └┘ └┘ └────────┘ └──┘
src └────────┘ └──┘
typ └─┘ └┘ └┘ └┘ └┘ └────────┘ └──┘
462
463 lemma is_O.prod_left_fst (h : is_O (λ x, (f' x, g' x)) k' l) : is_O f' k' l :=
id └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
464 is_O_fst_prod.trans h
id └───────────┘└────┘ ┴
src └───────────┘└────┘
typ └───────────┘└────┘ ┴
465
466 lemma is_O.prod_left_snd (h : is_O (λ x, (f' x, g' x)) k' l) : is_O g' k' l :=
id └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
467 is_O_snd_prod.trans h
id └───────────┘└────┘ ┴
src └───────────┘└────┘
typ └───────────┘└────┘ ┴
468
469 @[simp] lemma is_O_prod_left :
doc └──┘
470 is_O (λ x, (f' x, g' x)) k' l ↔ is_O f' k' l ∧ is_O g' k' l :=
id └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ ┴ └──┘ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘ └──┘
471 ⟨λ h, ⟨h.prod_left_fst, h.prod_left_snd⟩, λ h, h.1.prod_left h.2⟩
id ┴ ┴└────────────┘ ┴└────────────┘ ┴ ┴┴ └───────┘ ┴┴
src └────────────┘ └────────────┘ ┴ └───────┘ ┴
typ ┴ ┴└────────────┘ ┴└────────────┘ ┴ ┴┴ └───────┘ ┴┴
472
473 lemma is_o.prod_left (hf : is_o f' k' l) (hg : is_o g' k' l) : is_o (λ x, (f' x, g' x)) k' l :=
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴
doc └──┘ └──┘ └──┘
474 λ c hc, (hf hc).prod_left_same (hg hc)
id ┴ └┘ └┘ └┘ └────────────┘ └┘ └┘
src └────────────┘
typ ┴ └┘ └┘ └┘ └────────────┘ └┘ └┘
475
476 lemma is_o.prod_left_fst (h : is_o (λ x, (f' x, g' x)) k' l) : is_o f' k' l :=
id └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
477 is_O_fst_prod.trans_is_o h
id └───────────┘└─────────┘ ┴
src └───────────┘└─────────┘
typ └───────────┘└─────────┘ ┴
478
479 lemma is_o.prod_left_snd (h : is_o (λ x, (f' x, g' x)) k' l) : is_o g' k' l :=
id └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
480 is_O_snd_prod.trans_is_o h
id └───────────┘└─────────┘ ┴
src └───────────┘└─────────┘
typ └───────────┘└─────────┘ ┴
481
482 @[simp] lemma is_o_prod_left :
doc └──┘
483 is_o (λ x, (f' x, g' x)) k' l ↔ is_o f' k' l ∧ is_o g' k' l :=
id └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
src └──┘ ┴ ┴ └──┘ ┴ └──┘
typ └──┘ ┴ ┴└┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘ └┘ └┘ ┴ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘ └──┘
484 ⟨λ h, ⟨h.prod_left_fst, h.prod_left_snd⟩, λ h, h.1.prod_left h.2⟩
id ┴ ┴└────────────┘ ┴└────────────┘ ┴ ┴┴ └───────┘ ┴┴
src └────────────┘ └────────────┘ ┴ └───────┘ ┴
typ ┴ ┴└────────────┘ ┴└────────────┘ ┴ ┴┴ └───────┘ ┴┴
485
486 /-! ### Addition and subtraction -/
487
488 section add_sub
489
490 variables {c₁ c₂ : ℝ} {f₁ f₂ : α → E'}
id ┴
src ┴
typ ┴
491
492 theorem is_O_with.add (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_O_with c₂ f₂ g l) :
id └───────┘ └┘ └┘ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴
src └───────┘ └───────┘
typ └───────┘ └┘ └┘ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴
doc └───────┘ └───────┘
493 is_O_with (c₁ + c₂) (λ x, f₁ x + f₂ x) g l :=
id └───────┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
494 by filter_upwards [h₁, h₂] λ x hx₁ hx₂,
src └──────────────┘ └┘ └┘ └──────────┘
typ └──────────────┘ └┘ └┘ └──────────┘
doc └──────────────┘ └┘ └┘ └──────────┘
txt └──────────────┘ └┘ └┘ └──────────┘
par └──────────────┘ └┘ └┘ └──────────┘
pid └┘ └┘ ┴┴ └──────────┘
st └─────────────────────────────────────
495 calc ∥f₁ x + f₂ x∥ ≤ c₁ * ∥g x∥ + c₂ * ∥g x∥ : norm_add_le_of_le hx₁ hx₂
id ┴└┘ ┴ └┘ ┴ ┴ └───────────────┘
src ┴┴ ┴ ┴┴┴ ┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└───────────────┘┴ ┴ └
typ ┴┴└┘┴ ┴┴┴└┘┴ ┴┴ ┴ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└───────────────┘┴ ┴ └
doc ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └
txt ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └
par ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └
pid ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └
st ─────────────────────────────────────────────────────────────────────────
496 ... = (c₁ + c₂) * ∥g x∥ : (add_mul _ _ _).symm
id └┘ └┘ ┴ └─────┘
src ──────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ └─────┘└────────────
typ ──────────────────┘ ┴ └┘┴ ┴└┘└┘ ┴ ┴┴ └───────┘ └─────┘└────────────
doc ──────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ └────────────
txt ──────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ └────────────
par ──────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ └────────────
pid ──────────────────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ └─────────┘└─
st ────────────────────────────────────────────────────────────────────
497
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
498 theorem is_O.add : is_O f₁ g l → is_O f₂ g l → is_O (λ x, f₁ x + f₂ x) g l
id └──┘ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
499 | ⟨c₁, hc₁⟩ ⟨c₂, hc₂⟩ := (hc₁.add hc₂).is_O
id └─┘ └─┘ └──┘ └──┘
src └──┘ └──┘
typ └─┘ └─┘ └──┘ └──┘
500
501 theorem is_o.add (h₁ : is_o f₁ g l) (h₂ : is_o f₂ g l) : is_o (λ x, f₁ x + f₂ x) g l :=
id └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
502 λ c cpos, ((h₁ $ half_pos cpos).add (h₂ $ half_pos cpos)).congr_const (add_halves c)
id ┴ └──┘ └┘ └──────┘ └──┘ └─┘ └┘ └──────┘ └──┘ └─────────┘ └────────┘ ┴
src └──────┘ └─┘ └──────┘ └─────────┘ └────────┘
typ ┴ └──┘ └┘ └──────┘ └──┘ └─┘ └┘ └──────┘ └──┘ └─────────┘ └────────┘ ┴
503
504 theorem is_O.add_is_o (h₁ : is_O f₁ g l) (h₂ : is_o f₂ g l) : is_O (λ x, f₁ x + f₂ x) g l :=
id └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
505 h₁.add h₂.is_O
id └┘└──┘ └┘└───┘
src └──┘ └───┘
typ └┘└──┘ └┘└───┘
506
507 theorem is_o.add_is_O (h₁ : is_o f₁ g l) (h₂ : is_O f₂ g l) : is_O (λ x, f₁ x + f₂ x) g l :=
id └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
508 h₁.is_O.add h₂
id └┘└───┘└──┘ └┘
src └───┘└──┘
typ └┘└───┘└──┘ └┘
509
510 theorem is_O_with.add_is_o (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_o f₂ g l) (hc : c₁ < c₂) :
id └───────┘ └┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ └┘
src └───────┘ └──┘ ┴
typ └───────┘ └┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ └┘
doc └───────┘ └──┘
511 is_O_with c₂ (λx, f₁ x + f₂ x) g l :=
id └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
512 (h₁.add (h₂ (sub_pos.2 hc))).congr_const (add_sub_cancel'_right _ _)
id └┘└──┘ └┘ └─────┘┴ └┘ └─────────┘ └───────────────────┘
src └──┘ └─────┘┴ └─────────┘ └───────────────────┘
typ └┘└──┘ └┘ └─────┘┴ └┘ └─────────┘ └───────────────────┘
513
514 theorem is_o.add_is_O_with (h₁ : is_o f₁ g l) (h₂ : is_O_with c₁ f₂ g l) (hc : c₁ < c₂) :
id └──┘ └┘ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴ └┘ ┴ └┘
src └──┘ └───────┘ ┴
typ └──┘ └┘ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴ └┘ ┴ └┘
doc └──┘ └───────┘
515 is_O_with c₂ (λx, f₁ x + f₂ x) g l :=
id └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
516 (h₂.add_is_o h₁ hc).congr_left $ λ _, add_comm _ _
id └┘└───────┘ └┘ └┘ └────────┘ ┴ └──────┘
src └───────┘ └────────┘ └──────┘
typ └┘└───────┘ └┘ └┘ └────────┘ ┴ └──────┘
517
518 theorem is_O_with.sub (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_O_with c₂ f₂ g l) :
id └───────┘ └┘ └┘ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴
src └───────┘ └───────┘
typ └───────┘ └┘ └┘ ┴ ┴ └───────┘ └┘ └┘ ┴ ┴
doc └───────┘ └───────┘
519 is_O_with (c₁ + c₂) (λ x, f₁ x - f₂ x) g l :=
id └───────┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
520 h₁.add h₂.neg_left
id └┘└──┘ └┘└───────┘
src └──┘
typ └┘└──┘ └┘└───────┘
doc └───────┘
521
522 theorem is_O_with.sub_is_o (h₁ : is_O_with c₁ f₁ g l) (h₂ : is_o f₂ g l) (hc : c₁ < c₂) :
id └───────┘ └┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ └┘
src └───────┘ └──┘ ┴
typ └───────┘ └┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └┘ ┴ └┘
doc └───────┘ └──┘
523 is_O_with c₂ (λ x, f₁ x - f₂ x) g l :=
id └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
524 h₁.add_is_o h₂.neg_left hc
id └┘└───────┘ └┘└───────┘ └┘
src └───────┘
typ └┘└───────┘ └┘└───────┘ └┘
doc └───────┘
525
526 theorem is_O.sub (h₁ : is_O f₁ g l) (h₂ : is_O f₂ g l) : is_O (λ x, f₁ x - f₂ x) g l :=
id └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
527 h₁.add h₂.neg_left
id └┘└──┘ └┘└───────┘
src └──┘
typ └┘└──┘ └┘└───────┘
doc └───────┘
528
529 theorem is_o.sub (h₁ : is_o f₁ g l) (h₂ : is_o f₂ g l) : is_o (λ x, f₁ x - f₂ x) g l :=
id └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ └──┘ └──┘ ┴
typ └──┘ └┘ ┴ ┴ └──┘ └┘ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘ └──┘
530 h₁.add h₂.neg_left
id └┘└──┘ └┘└───────┘
src └──┘
typ └┘└──┘ └┘└───────┘
doc └───────┘
531
532 end add_sub
533
534 /-! ### Lemmas about `is_O (f₁ - f₂) g l` / `is_o (f₁ - f₂) g l` treated as a binary relation -/
535
536 section is_oO_as_rel
537
538 variables {f₁ f₂ f₃ : α → E'}
539
540 theorem is_O_with.symm (h : is_O_with c (λ x, f₁ x - f₂ x) g l) :
id └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
541 is_O_with c (λ x, f₂ x - f₁ x) g l :=
id └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
542 h.neg_left.congr_left $ λ x, neg_sub _ _
id ┴└───────┘└─────────┘ ┴ └─────┘
src └─────────┘ └─────┘
typ ┴└───────┘└─────────┘ ┴ └─────┘
doc └───────┘
543
544 theorem is_O_with_comm :
545 is_O_with c (λ x, f₁ x - f₂ x) g l ↔ is_O_with c (λ x, f₂ x - f₁ x) g l :=
id └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └───────┘ ┴
typ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘ └───────┘
546 ⟨is_O_with.symm, is_O_with.symm⟩
id └────────────┘ └────────────┘
src └────────────┘ └────────────┘
typ └────────────┘ └────────────┘
547
548 theorem is_O.symm (h : is_O (λ x, f₁ x - f₂ x) g l) : is_O (λ x, f₂ x - f₁ x) g l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴ └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘
549 h.neg_left.congr_left $ λ x, neg_sub _ _
id ┴└───────┘└─────────┘ ┴ └─────┘
src └─────────┘ └─────┘
typ ┴└───────┘└─────────┘ ┴ └─────┘
doc └───────┘
550
551 theorem is_O_comm : is_O (λ x, f₁ x - f₂ x) g l ↔ is_O (λ x, f₂ x - f₁ x) g l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘
552 ⟨is_O.symm, is_O.symm⟩
id └───────┘ └───────┘
src └───────┘ └───────┘
typ └───────┘ └───────┘
553
554 theorem is_o.symm (h : is_o (λ x, f₁ x - f₂ x) g l) : is_o (λ x, f₂ x - f₁ x) g l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴ └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘
555 by simpa only [neg_sub] using h.neg_left
id └─────┘ └────────┘
src └──────────┘└─────┘└──────┘ └
typ └──────────┘└─────┘└──────┘└────────┘└
doc └──────────┘ └──────┘└────────┘└
txt └──────────┘ └──────┘ └
par └──────────┘ └──────┘ └
pid ┴└──┘└┘ ┴┴└────┘ └
st └──────────────────────────────────────
556
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
557 theorem is_o_comm : is_o (λ x, f₁ x - f₂ x) g l ↔ is_o (λ x, f₂ x - f₁ x) g l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘
558 ⟨is_o.symm, is_o.symm⟩
id └───────┘ └───────┘
src └───────┘ └───────┘
typ └───────┘ └───────┘
559
560 theorem is_O_with.triangle (h₁ : is_O_with c (λ x, f₁ x - f₂ x) g l)
id └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
561 (h₂ : is_O_with c' (λ x, f₂ x - f₃ x) g l) :
id └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
562 is_O_with (c + c') (λ x, f₁ x - f₃ x) g l :=
id └───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └───────┘
563 (h₁.add h₂).congr_left $ λ x, sub_add_sub_cancel _ _ _
id └┘└──┘ └┘ └────────┘ ┴ └────────────────┘
src └──┘ └────────┘ └────────────────┘
typ └┘└──┘ └┘ └────────┘ ┴ └────────────────┘
564
565 theorem is_O.triangle (h₁ : is_O (λ x, f₁ x - f₂ x) g l) (h₂ : is_O (λ x, f₂ x - f₃ x) g l) :
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴ └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘
566 is_O (λ x, f₁ x - f₃ x) g l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘
567 (h₁.add h₂).congr_left $ λ x, sub_add_sub_cancel _ _ _
id └┘└──┘ └┘ └────────┘ ┴ └────────────────┘
src └──┘ └────────┘ └────────────────┘
typ └┘└──┘ └┘ └────────┘ ┴ └────────────────┘
568
569 theorem is_o.triangle (h₁ : is_o (λ x, f₁ x - f₂ x) g l) (h₂ : is_o (λ x, f₂ x - f₃ x) g l) :
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴ └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘ └──┘
570 is_o (λ x, f₁ x - f₃ x) g l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘
571 (h₁.add h₂).congr_left $ λ x, sub_add_sub_cancel _ _ _
id └┘└──┘ └┘ └────────┘ ┴ └────────────────┘
src └──┘ └────────┘ └────────────────┘
typ └┘└──┘ └┘ └────────┘ ┴ └────────────────┘
572
573 theorem is_O.congr_of_sub (h : is_O (λ x, f₁ x - f₂ x) g l) :
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘
574 is_O f₁ g l ↔ is_O f₂ g l :=
id └──┘ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ └──┘
typ └──┘ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘
575 ⟨λ h', (h'.sub h).congr_left (λ x, sub_sub_cancel _ _),
id └┘ └┘└──┘ ┴ └────────┘ ┴ └────────────┘
src └──┘ └────────┘ └────────────┘
typ └┘ └┘└──┘ ┴ └────────┘ ┴ └────────────┘
576 λ h', (h.add h').congr_left (λ x, sub_add_cancel _ _)⟩
id └┘ ┴└──┘ └┘ └────────┘ ┴ └────────────┘
src └──┘ └────────┘ └────────────┘
typ └┘ ┴└──┘ └┘ └────────┘ ┴ └────────────┘
577
578 theorem is_o.congr_of_sub (h : is_o (λ x, f₁ x - f₂ x) g l) :
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘
579 is_o f₁ g l ↔ is_o f₂ g l :=
id └──┘ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ └──┘
typ └──┘ └┘ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘
580 ⟨λ h', (h'.sub h).congr_left (λ x, sub_sub_cancel _ _),
id └┘ └┘└──┘ ┴ └────────┘ ┴ └────────────┘
src └──┘ └────────┘ └────────────┘
typ └┘ └┘└──┘ ┴ └────────┘ ┴ └────────────┘
581 λ h', (h.add h').congr_left (λ x, sub_add_cancel _ _)⟩
id └┘ ┴└──┘ └┘ └────────┘ ┴ └────────────┘
src └──┘ └────────┘ └────────────┘
typ └┘ ┴└──┘ └┘ └────────┘ ┴ └────────────┘
582
583 end is_oO_as_rel
584
585 /-! ### Zero, one, and other constants -/
586
587 section zero_const
588
589 variables (g' l)
590
591 theorem is_o_zero : is_o (λ x, (0 : E')) g' l :=
id └──┘ ┴ └┘ └┘ ┴
src └──┘
typ └──┘ ┴ └┘ └┘ ┴
doc └──┘
592 λ c hc, univ_mem_sets' $ λ x, by simpa using mul_nonneg (le_of_lt hc) (norm_nonneg $ g' x)
id ┴ └┘ └────────────┘ ┴ └────────┘ └──────┘ └┘ └─────────┘ └┘ ┴
src └────────────┘ └──────────┘└────────┘┴ └──────┘┴ └┘ └─────────┘┴ ┴ ┴ └─
typ ┴ └┘ └────────────┘ ┴ └──────────┘└────────┘┴ └──────┘┴└┘└┘ └─────────┘┴ ┴└┘┴┴└─
doc └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─
txt └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─
par └──────────┘ ┴ ┴ └┘ ┴ ┴ ┴ └─
pid ┴└────┘ ┴ ┴ └┘ ┴ ┴ ┴ ┴└
st └──────────────────────────────────────────────────────────
593
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
594 theorem is_O_with_zero (hc : 0 < c) : is_O_with c (λ x, (0 : E')) g' l :=
id ┴ ┴ └───────┘ ┴ ┴ └┘ └┘ ┴
src ┴ └───────┘
typ ┴ ┴ └───────┘ ┴ ┴ └┘ └┘ ┴
doc └───────┘
595 (is_o_zero g' l) hc
id └───────┘ └┘ ┴ └┘
src └───────┘
typ └───────┘ └┘ ┴ └┘
596
597 theorem is_O_zero : is_O (λ x, (0 : E')) g' l := (is_o_zero g' l).is_O
id └──┘ ┴ └┘ └┘ ┴ └───────┘ └┘ ┴ └──┘
src └──┘ └───────┘ └──┘
typ └──┘ ┴ └┘ └┘ ┴ └───────┘ └┘ ┴ └──┘
doc └──┘
598
599 theorem is_O_refl_left : is_O (λ x, f' x - f' x) g' l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
src └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
doc └──┘
600 (is_O_zero g' l).congr_left $ λ x, (sub_self _).symm
id └───────┘ └┘ ┴ └────────┘ ┴ └──────┘ └──┘
src └───────┘ └────────┘ └──────┘ └──┘
typ └───────┘ └┘ ┴ └────────┘ ┴ └──────┘ └──┘
601
602 theorem is_o_refl_left : is_o (λ x, f' x - f' x) g' l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
src └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴
doc └──┘
603 (is_o_zero g' l).congr_left $ λ x, (sub_self _).symm
id └───────┘ └┘ ┴ └────────┘ ┴ └──────┘ └──┘
src └───────┘ └────────┘ └──────┘ └──┘
typ └───────┘ └┘ ┴ └────────┘ ┴ └──────┘ └──┘
604
605 variables {g' l}
606
607 theorem is_O_with_zero_right_iff :
608 is_O_with c f' (λ x, (0 : F')) l ↔ ∀ᶠ x in l, f' x = 0 :=
id └───────┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
src └───────┘ ┴ └┘ └┘ ┴ ┴
typ └───────┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
doc └───────┘ └┘ └┘ ┴
609 by simp only [is_O_with, exists_prop, true_and, norm_zero, mul_zero, norm_le_zero_iff]
id └───────┘ └─────────┘ └──────┘ └───────┘ └──────┘ └──────────────┘
src └─────────┘└───────┘└┘└─────────┘└┘└──────┘└┘└───────┘└┘└──────┘└┘└──────────────┘└─
typ └─────────┘└───────┘└┘└─────────┘└┘└──────┘└┘└───────┘└┘└──────┘└┘└──────────────┘└─
doc └─────────┘└───────┘└┘ └┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────────
610
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
611 theorem is_O_zero_right_iff : is_O f' (λ x, (0 : F')) l ↔ ∀ᶠ x in l, f' x = 0 :=
id └──┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
src └──┘ ┴ └┘ └┘ ┴ ┴
typ └──┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
doc └──┘ └┘ └┘ ┴
612 ⟨λ h, let ⟨c, hc⟩ := h in (is_O_with_zero_right_iff).1 hc,
id ┴ └─┘ └┘ ┴ └──────────────────────┘ ┴
src └──────────────────────┘ ┴
typ ┴ └─┘ └┘ ┴ └──────────────────────┘ ┴
613 λ h, (is_O_with_zero_right_iff.2 h : is_O_with 1 _ _ _).is_O⟩
id ┴ └──────────────────────┘┴ ┴ └───────┘ └──┘
src └──────────────────────┘┴ └───────┘ └──┘
typ ┴ └──────────────────────┘┴ ┴ └───────┘ └──┘
doc └───────┘
614
615 theorem is_o_zero_right_iff :
616 is_o f' (λ x, (0 : F')) l ↔ ∀ᶠ x in l, f' x = 0 :=
id └──┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
src └──┘ ┴ └┘ └┘ ┴ ┴
typ └──┘ └┘ ┴ └┘ ┴ ┴ └┘ ┴ └┘ ┴┴ └┘ ┴ ┴
doc └──┘ └┘ └┘ ┴
617 ⟨λ h, is_O_zero_right_iff.1 h.is_O,
id ┴ └─────────────────┘┴ ┴└───┘
src └─────────────────┘┴ └───┘
typ ┴ └─────────────────┘┴ ┴└───┘
618 λ h c hc, is_O_with_zero_right_iff.2 h⟩
id ┴ ┴ └┘ └──────────────────────┘┴ ┴
src └──────────────────────┘┴
typ ┴ ┴ └┘ └──────────────────────┘┴ ┴
619
620 theorem is_O_with_const_const (c : E) {c' : F'} (hc' : c' ≠ 0) (l : filter α) :
id ┴ └┘ └┘ ┴ └────┘ ┴
src ┴ └────┘
typ ┴ └┘ └┘ ┴ └────┘ ┴
621 is_O_with (∥c∥ / ∥c'∥) (λ x : α, c) (λ x, c') l :=
id └───────┘ ┴┴┴ ┴ ┴└┘┴ ┴ ┴ ┴ └┘ ┴
src └───────┘ ┴ ┴ ┴ ┴ ┴
typ └───────┘ ┴┴┴ ┴ ┴└┘┴ ┴ ┴ ┴ └┘ ┴
doc └───────┘
622 begin
st └─────
623 apply univ_mem_sets',
id └────────────┘
src └────┘└────────────┘
typ └────┘└────────────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────────┘└─
624 intro x,
src └─────┘
typ └─────┘
doc └─────┘
txt └─────┘
par └─────┘
pid └┘
st ────────┘└─
625 rw [mem_set_of_eq, div_mul_cancel],
id └───────────┘ └────────────┘
src └──┘└───────────┘└┘└────────────┘┴
typ └──┘└───────────┘└┘└────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────┘└──────────────┘└──
626 rwa [ne.def, norm_eq_zero]
id └────┘ └──────────┘
src └───┘└────┘└┘└──────────┘└┘
typ └───┘└────┘└┘└──────────┘└┘
doc └───┘ └┘ └┘
txt └───┘ └┘ └┘
par └───┘ └┘ └┘
pid └┘ └┘ ┴┴
st ────────────┘└────────────┘┴┴
627 end
st └─┘
628
629 theorem is_O_const_const (c : E) {c' : F'} (hc' : c' ≠ 0) (l : filter α) :
id ┴ └┘ └┘ ┴ └────┘ ┴
src ┴ └────┘
typ ┴ └┘ └┘ ┴ └────┘ ┴
630 is_O (λ x : α, c) (λ x, c') l :=
id └──┘ ┴ ┴ ┴ └┘ ┴
src └──┘
typ └──┘ ┴ ┴ ┴ └┘ ┴
doc └──┘
631 (is_O_with_const_const c hc' l).is_O
id └───────────────────┘ ┴ └─┘ ┴ └──┘
src └───────────────────┘ └──┘
typ └───────────────────┘ ┴ └─┘ ┴ └──┘
632
633 end zero_const
634
635 theorem is_O_with_const_one (c : E) (l : filter α) : is_O_with ∥c∥ (λ x : α, c) (λ x, (1 : 𝕜)) l :=
id ┴ └────┘ ┴ └───────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
src └────┘ └───────┘ ┴ ┴
typ ┴ └────┘ ┴ └───────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
636 begin
st └─────
637 refine (is_O_with_const_const c _ l).congr_const _,
id └───────────────────┘ ┴ ┴
src └─────┘ └───────────────────┘┴ └─┘ └─────────────┘
typ └─────┘ └───────────────────┘┴┴└─┘┴└─────────────┘
doc └─────┘ ┴ └─┘ └─────────────┘
txt └─────┘ ┴ └─┘ └─────────────┘
par └─────┘ ┴ └─┘ └─────────────┘
pid ┴ ┴ └─┘ └─────────────┘
st ───────────────────────────────────────────────────┘└─
638 { rw [normed_field.norm_one, div_one] },
id └───────────────────┘ └─────┘
src └──┘└───────────────────┘└┘└─────┘└┘
typ └──┘└───────────────────┘└┘└─────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───┘└───────────────────────┘└───────┘┴┴└┘└
639 { exact one_ne_zero }
id └─────────┘
src └────┘└─────────┘┴
typ └────┘└─────────┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────────────────────┘└─
640 end
st ──┘
641
642 theorem is_O_const_one (c : E) (l : filter α) : is_O (λ x : α, c) (λ x, (1 : 𝕜)) l :=
id ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
src └────┘ └──┘
typ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
643 (is_O_with_const_one c l).is_O
id └─────────────────┘ ┴ ┴ └──┘
src └─────────────────┘ └──┘
typ └─────────────────┘ ┴ ┴ └──┘
644
645 section
646
647 variable (𝕜)
648
649 theorem is_o_const_iff_is_o_one {c : F'} (hc : c ≠ 0) :
id └┘ ┴ ┴
src ┴
typ └┘ ┴ ┴
650 is_o f (λ x, c) l ↔ is_o f (λ x, (1:𝕜)) l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘ └──┘
651 ⟨λ h, h.trans_is_O $ is_O_const_one c l, λ h, h.trans_is_O $ is_O_const_const _ hc _⟩
id ┴ ┴└─────────┘ └────────────┘ ┴ ┴ ┴ ┴└─────────┘ └──────────────┘ └┘
src └─────────┘ └────────────┘ └─────────┘ └──────────────┘
typ ┴ ┴└─────────┘ └────────────┘ ┴ ┴ ┴ ┴└─────────┘ └──────────────┘ └┘
652
653 end
654
655 theorem is_o_const_iff {c : F'} (hc : c ≠ 0) :
id └┘ ┴ ┴
src ┴
typ └┘ ┴ ┴
656 is_o f' (λ x, c) l ↔ tendsto f' l (𝓝 0) :=
id └──┘ └┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
src └──┘ ┴ └─────┘ ┴
typ └──┘ └┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
doc └──┘ └─────┘ ┴
657 (is_o_const_iff_is_o_one ℝ hc).trans
id └─────────────────────┘ ┴ └┘ └───┘
src └─────────────────────┘ ┴ └───┘
typ └─────────────────────┘ ┴ └┘ └───┘
658 begin
st └─────
659 clear hc c,
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid └───┘
st ───────────┘└─
660 simp only [is_o, is_O_with, normed_field.norm_one, mul_one, normed_group.tendsto_nhds_zero],
id └──┘ └───────┘ └───────────────────┘ └─────┘ └────────────────────────────┘
src └─────────┘└──┘└┘└───────┘└┘└───────────────────┘└┘└─────┘└┘└────────────────────────────┘┴
typ └─────────┘└──┘└┘└───────┘└┘└───────────────────┘└┘└─────┘└┘└────────────────────────────┘┴
doc └─────────┘└──┘└┘└───────┘└┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘└─
661 -- Now the only difference is `≤` vs `<`
st ───────────────────────────────────────────
662 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
663 { intros h ε hε0,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ───┘└────────────┘└─
664 apply mem_sets_of_superset (h (half_pos hε0)),
id └──────────────────┘ ┴ └──────┘ └─┘
src └────┘└──────────────────┘┴ ┴ └──────┘┴ └┘
typ └────┘└──────────────────┘┴ ┴┴ └──────┘┴└─┘└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ └┘
st ────────────────────────────────────────────────┘└─
665 intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
666 simp only [mem_set_of_eq] at hx ⊢,
id └───────────┘
src └─────────┘└───────────┘└───────┘
typ └─────────┘└───────────┘└───────┘
doc └─────────┘ └───────┘
txt └─────────┘ └───────┘
par └─────────┘ └───────┘
pid ┴└──┘└┘ ┴┴└─────┘
st ────────────────────────────────────┘└─
667 exact lt_of_le_of_lt hx (half_lt_self hε0) },
id └────────────┘ └┘ └──────────┘ └─┘
src └────┘└────────────┘┴ ┴ └──────────┘┴ └┘
typ └────┘└────────────┘┴└┘┴ └──────────┘┴└─┘└┘
doc └────┘ ┴ ┴ ┴ └┘
txt └────┘ ┴ ┴ ┴ └┘
par └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴ ┴┴
st ──────────────────────────────────────────────┘└┘└
668 { intros h ε hε0,
src └────────────┘
typ └────────────┘
doc └────────────┘
txt └────────────┘
par └────────────┘
pid └──────┘
st ─────────────────┘└─
669 apply mem_sets_of_superset (h ε hε0),
id └──────────────────┘ ┴ ┴ └─┘
src └────┘└──────────────────┘┴ ┴ ┴ ┴
typ └────┘└──────────────────┘┴ ┴┴┴┴└─┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────┘└─
670 intros x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └───┘
st ──────────────┘└─
671 simp only [mem_set_of_eq] at hx ⊢,
id └───────────┘
src └─────────┘└───────────┘└───────┘
typ └─────────┘└───────────┘└───────┘
doc └─────────┘ └───────┘
txt └─────────┘ └───────┘
par └─────────┘ └───────┘
pid ┴└──┘└┘ ┴┴└─────┘
st ────────────────────────────────────┘└─
672 exact le_of_lt hx }
id └──────┘ └┘
src └────┘└──────┘┴ ┴
typ └────┘└──────┘┴└┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────────────────────┘└─
673 end
st ──┘
674
675 theorem is_O_const_of_tendsto {y : E'} (h : tendsto f' l (𝓝 y)) {c : F'} (hc : c ≠ 0) :
id └┘ └─────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴
src └─────┘ ┴ ┴
typ └┘ └─────┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴
doc └─────┘ ┴
676 is_O f' (λ x, c) l :=
id └──┘ └┘ ┴ ┴ ┴
src └──┘
typ └──┘ └┘ ┴ ┴ ┴
doc └──┘
677 begin
st └─────
678 refine is_O.trans _ (is_O_const_const (∥y∥ + 1) hc l),
id └────────┘ └──────────────┘ ┴┴┴ ┴ └┘ ┴
src └─────┘└────────┘└─┘ └──────────────┘┴ ┴ ┴┴┴└──┘ ┴ ┴
typ └─────┘└────────┘└─┘ └──────────────┘┴ ┴┴┴┴┴└──┘└┘┴┴┴
doc └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴
txt └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴
par └─────┘ └─┘ ┴ ┴ └──┘ ┴ ┴
pid ┴ └─┘ ┴ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────────────────┘└─
679 use 1,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴┴
st ──────┘└─
680 simp only [is_O_with, one_mul],
id └───────┘ └─────┘
src └─────────┘└───────┘└┘└─────┘┴
typ └─────────┘└───────┘└┘└─────┘┴
doc └─────────┘└───────┘└┘ ┴
txt └─────────┘ └┘ ┴
par └─────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st ───────────────────────────────┘└─
681 have : tendsto (λx, ∥f' x∥) l (𝓝 ∥y∥), from (continuous_norm.tendsto _).comp h,
id └─────┘ └┘ ┴ ┴ ┴ └─────────────────────┘ ┴
src └─────┘└─────┘┴ └─┘ ┴ └┘ ┴ ┴┴ ┴ └───┘ └─────────────────────┘└───────┘
typ └─────┘└─────┘┴ └─┘ └┘┴ └┘┴┴ ┴┴ ┴ ┴ └───┘ └─────────────────────┘└───────┘┴
doc └─────┘└─────┘┴ └─┘ ┴ └┘ ┴ ┴┴ ┴ └───┘ └───────┘
txt └─────┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └───┘ └───────┘
par └─────┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └───┘ └───────┘
pid └───┘└┘ ┴ └─┘ ┴ └┘ ┴ ┴ ┴ └───┘ └───────┘
st ──────────────────────────────────────┘└───────────────────────────────────────┘└─
682 have Iy : ∥y∥ < ∥∥y∥ + 1∥, from lt_of_lt_of_le (lt_add_one _) (le_abs_self _),
id ┴ ┴ └────────────┘ └────────┘ └─────────┘
src └────────┘ ┴┴┴ ┴ └┘ └───┘└────────────┘┴ └────────┘└──┘ └─────────┘└─┘
typ └────────┘ ┴┴┴ ┴ ┴ └┘ └───┘└────────────┘┴ └────────┘└──┘ └─────────┘└─┘
doc └────────┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └─┘
txt └────────┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └─┘
par └────────┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └─┘
pid └─────┘└─┘ ┴ ┴ ┴ └┘ └───┘ ┴ └──┘ └─┘
st ──────────────────────────┘└──────────────────────────────────────────────────┘└─
683 exact this (ge_mem_nhds Iy)
id └──┘ └─────────┘ └┘
src └────┘ ┴ └─────────┘┴ └┘
typ └────┘└──┘┴ └─────────┘┴└┘└┘
doc └────┘ ┴ ┴ └┘
txt └────┘ ┴ ┴ └┘
par └────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ ┴┴
st ─────────────────────────────┘
684 end
st └─┘
685
686 section
687
688 variable (𝕜)
689
690 theorem is_o_one_iff : is_o f' (λ x, (1 : 𝕜)) l ↔ tendsto f' l (𝓝 0) :=
id └──┘ └┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
src └──┘ ┴ └─────┘ ┴
typ └──┘ └┘ ┴ ┴ ┴ ┴ └─────┘ └┘ ┴ ┴
doc └──┘ └─────┘ ┴
691 is_o_const_iff one_ne_zero
id └────────────┘ └─────────┘
src └────────────┘ └─────────┘
typ └────────────┘ └─────────┘
692
693 theorem is_O_one_of_tendsto {y : E'} (h : tendsto f' l (𝓝 y)) :
id └┘ └─────┘ └┘ ┴ ┴ ┴
src └─────┘ ┴
typ └┘ └─────┘ └┘ ┴ ┴ ┴
doc └─────┘ ┴
694 is_O f' (λ x, (1:𝕜)) l :=
id └──┘ └┘ ┴ ┴ ┴
src └──┘
typ └──┘ └┘ ┴ ┴ ┴
doc └──┘
695 is_O_const_of_tendsto h one_ne_zero
id └───────────────────┘ ┴ └─────────┘
src └───────────────────┘ └─────────┘
typ └───────────────────┘ ┴ └─────────┘
696
697 theorem is_O.trans_tendsto_nhds (hfg : is_O f g' l) {y : F'} (hg : tendsto g' l (𝓝 y)) :
id └──┘ ┴ └┘ ┴ └┘ └─────┘ └┘ ┴ ┴ ┴
src └──┘ └─────┘ ┴
typ └──┘ ┴ └┘ ┴ └┘ └─────┘ └┘ ┴ ┴ ┴
doc └──┘ └─────┘ ┴
698 is_O f (λ x, (1:𝕜)) l :=
id └──┘ ┴ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴ ┴
doc └──┘
699 hfg.trans $ is_O_one_of_tendsto 𝕜 hg
id └─┘└────┘ └─────────────────┘ ┴ └┘
src └────┘ └─────────────────┘
typ └─┘└────┘ └─────────────────┘ ┴ └┘
700
701 end
702
703 theorem is_O.trans_tendsto (hfg : is_O f' g' l) (hg : tendsto g' l (𝓝 0)) :
id └──┘ └┘ └┘ ┴ └─────┘ └┘ ┴ ┴
src └──┘ └─────┘ ┴
typ └──┘ └┘ └┘ ┴ └─────┘ └┘ ┴ ┴
doc └──┘ └─────┘ ┴
704 tendsto f' l (𝓝 0) :=
id └─────┘ └┘ ┴ ┴
src └─────┘ ┴
typ └─────┘ └┘ ┴ ┴
doc └─────┘ ┴
705 (is_o_one_iff ℝ).1 $ hfg.trans_is_o $ (is_o_one_iff ℝ).2 hg
id └──────────┘ ┴ ┴ └─┘└─────────┘ └──────────┘ ┴ ┴ └┘
src └──────────┘ ┴ ┴ └─────────┘ └──────────┘ ┴ ┴
typ └──────────┘ ┴ ┴ └─┘└─────────┘ └──────────┘ ┴ ┴ └┘
706
707 theorem is_o.trans_tendsto (hfg : is_o f' g' l) (hg : tendsto g' l (𝓝 0)) :
id └──┘ └┘ └┘ ┴ └─────┘ └┘ ┴ ┴
src └──┘ └─────┘ ┴
typ └──┘ └┘ └┘ ┴ └─────┘ └┘ ┴ ┴
doc └──┘ └─────┘ ┴
708 tendsto f' l (𝓝 0) :=
id └─────┘ └┘ ┴ ┴
src └─────┘ ┴
typ └─────┘ └┘ ┴ ┴
doc └─────┘ ┴
709 hfg.is_O.trans_tendsto hg
id └─┘└───┘└────────────┘ └┘
src └───┘└────────────┘
typ └─┘└───┘└────────────┘ └┘
710
711 /-! ### Multiplication by a constant -/
712
713 theorem is_O_with_const_mul_self (c : R) (f : α → R) (l : filter α) :
id ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ └────┘ ┴
714 is_O_with ∥c∥ (λ x, c * f x) f l :=
id └───────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
715 is_O_with_of_le' _ $ λ x, norm_mul_le _ _
id └──────────────┘ ┴ └─────────┘
src └──────────────┘ └─────────┘
typ └──────────────┘ ┴ └─────────┘
716
717 theorem is_O_const_mul_self (c : R) (f : α → R) (l : filter α) :
id ┴ ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ ┴ └────┘ ┴
718 is_O (λ x, c * f x) f l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
719 (is_O_with_const_mul_self c f l).is_O
id └──────────────────────┘ ┴ ┴ ┴ └──┘
src └──────────────────────┘ └──┘
typ └──────────────────────┘ ┴ ┴ ┴ └──┘
720
721 theorem is_O_with.const_mul_left {f : α → R} (h : is_O_with c f g l) (c' : R) :
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
722 is_O_with (∥c'∥ * c) (λ x, c' * f x) g l :=
id └───────┘ ┴└┘┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴└┘┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └───────┘
723 (is_O_with_const_mul_self c' f l).trans h (norm_nonneg c')
id └──────────────────────┘ └┘ ┴ ┴ └───┘ ┴ └─────────┘ └┘
src └──────────────────────┘ └───┘ └─────────┘
typ └──────────────────────┘ └┘ ┴ ┴ └───┘ ┴ └─────────┘ └┘
724
725 theorem is_O.const_mul_left {f : α → R} (h : is_O f g l) (c' : R) :
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
726 is_O (λ x, c' * f x) g l :=
id └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ └┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
727 let ⟨c, hc⟩ := h in (hc.const_mul_left c').is_O
id └─┘ └┘ ┴ └─────────────┘ └┘ └──┘
src └─────────────┘ └──┘
typ └─┘ └┘ ┴ └─────────────┘ └┘ └──┘
728
729 theorem is_O_with_self_const_mul' (u : units R) (f : α → R) (l : filter α) :
id └───┘ ┴ ┴ ┴ └────┘ ┴
src └───┘ └────┘
typ └───┘ ┴ ┴ ┴ └────┘ ┴
730 is_O_with ∥(↑u⁻¹:R)∥ f (λ x, ↑u * f x) l :=
id └───────┘ ┴ ┴┴└┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ └┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴┴└┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └───────┘
731 (is_O_with_const_mul_self ↑u⁻¹ _ l).congr_left $ λ x, u.inv_mul_cancel_left (f x)
id └──────────────────────┘ ┴┴└┘ ┴ └────────┘ ┴ ┴└──────────────────┘ ┴ ┴
src └──────────────────────┘ ┴ └┘ └────────┘ └──────────────────┘
typ └──────────────────────┘ ┴┴└┘ ┴ └────────┘ ┴ ┴└──────────────────┘ ┴ ┴
732
733 theorem is_O_with_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : filter α) :
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴
src ┴ └────┘
typ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
734 is_O_with ∥c∥⁻¹ f (λ x, c * f x) l :=
id └───────┘ ┴┴┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴└┘ ┴
typ └───────┘ ┴┴┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
735 (is_O_with_self_const_mul' (units.mk0 c hc) f l).congr_const $
id └───────────────────────┘ └───────┘ ┴ └┘ ┴ ┴ └─────────┘
src └───────────────────────┘ └───────┘ └─────────┘
typ └───────────────────────┘ └───────┘ ┴ └┘ ┴ ┴ └─────────┘
doc └───────┘
736 normed_field.norm_inv c
id └───────────────────┘ ┴
src └───────────────────┘
typ └───────────────────┘ ┴
737
738 theorem is_O_self_const_mul' {c : R} (hc : is_unit c) (f : α → R) (l : filter α) :
id ┴ └─────┘ ┴ ┴ ┴ └────┘ ┴
src └─────┘ └────┘
typ ┴ └─────┘ ┴ ┴ ┴ └────┘ ┴
doc └─────┘
739 is_O f (λ x, c * f x) l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
740 let ⟨u, hu⟩ := hc in hu.symm ▸ (is_O_with_self_const_mul' u f l).is_O
id └─┘ ┴ └┘ └┘ └───┘ ┴ └───────────────────────┘ ┴ ┴ └──┘
src └───┘ ┴ └───────────────────────┘ └──┘
typ └─┘ ┴ └┘ └┘ └───┘ ┴ └───────────────────────┘ ┴ ┴ └──┘
741
742 theorem is_O_self_const_mul (c : 𝕜) (hc : c ≠ 0) (f : α → 𝕜) (l : filter α) :
id ┴ ┴ ┴ ┴ ┴ └────┘ ┴
src ┴ └────┘
typ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
743 is_O f (λ x, c * f x) l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
744 is_O_self_const_mul' (is_unit.mk0 c hc) f l
id └──────────────────┘ └─────────┘ ┴ └┘ ┴ ┴
src └──────────────────┘ └─────────┘
typ └──────────────────┘ └─────────┘ ┴ └┘ ┴ ┴
745
746 theorem is_O_const_mul_left_iff' {f : α → R} {c : R} (hc : is_unit c) :
id ┴ ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
747 is_O (λ x, c * f x) g l ↔ is_O f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
748 ⟨(is_O_self_const_mul' hc f l).trans, λ h, h.const_mul_left c⟩
id └──────────────────┘ └┘ ┴ ┴ └───┘ ┴ ┴└─────────────┘ ┴
src └──────────────────┘ └───┘ └─────────────┘
typ └──────────────────┘ └┘ ┴ ┴ └───┘ ┴ ┴└─────────────┘ ┴
749
750 theorem is_O_const_mul_left_iff {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
751 is_O (λ x, c * f x) g l ↔ is_O f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
752 is_O_const_mul_left_iff' $ is_unit.mk0 c hc
id └──────────────────────┘ └─────────┘ ┴ └┘
src └──────────────────────┘ └─────────┘
typ └──────────────────────┘ └─────────┘ ┴ └┘
753
754 theorem is_o.const_mul_left {f : α → R} (h : is_o f g l) (c : R) :
id ┴ ┴ └──┘ ┴ ┴ ┴ ┴
src └──┘
typ ┴ ┴ └──┘ ┴ ┴ ┴ ┴
doc └──┘
755 is_o (λ x, c * f x) g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
756 (is_O_const_mul_self c f l).trans_is_o h
id └─────────────────┘ ┴ ┴ ┴ └────────┘ ┴
src └─────────────────┘ └────────┘
typ └─────────────────┘ ┴ ┴ ┴ └────────┘ ┴
757
758 theorem is_o_const_mul_left_iff' {f : α → R} {c : R} (hc : is_unit c) :
id ┴ ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
759 is_o (λ x, c * f x) g l ↔ is_o f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
760 ⟨(is_O_self_const_mul' hc f l).trans_is_o, λ h, h.const_mul_left c⟩
id └──────────────────┘ └┘ ┴ ┴ └────────┘ ┴ ┴└─────────────┘ ┴
src └──────────────────┘ └────────┘ └─────────────┘
typ └──────────────────┘ └┘ ┴ ┴ └────────┘ ┴ ┴└─────────────┘ ┴
761
762 theorem is_o_const_mul_left_iff {f : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
763 is_o (λ x, c * f x) g l ↔ is_o f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
764 is_o_const_mul_left_iff' $ is_unit.mk0 c hc
id └──────────────────────┘ └─────────┘ ┴ └┘
src └──────────────────────┘ └─────────┘
typ └──────────────────────┘ └─────────┘ ┴ └┘
765
766 theorem is_O_with.of_const_mul_right {g : α → R} {c : R} (hc' : 0 ≤ c')
id ┴ ┴ ┴ ┴ └┘
src ┴
typ ┴ ┴ ┴ ┴ └┘
767 (h : is_O_with c' f (λ x, c * g x) l) :
id └───────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴
typ └───────┘ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
768 is_O_with (c' * ∥c∥) f g l :=
id └───────┘ └┘ ┴ ┴┴┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ └┘ ┴ ┴┴┴ ┴ ┴ ┴
doc └───────┘
769 h.trans (is_O_with_const_mul_self c g l) hc'
id ┴└────┘ └──────────────────────┘ ┴ ┴ ┴ └─┘
src └────┘ └──────────────────────┘
typ ┴└────┘ └──────────────────────┘ ┴ ┴ ┴ └─┘
770
771 theorem is_O.of_const_mul_right {g : α → R} {c : R}
id ┴ ┴ ┴
typ ┴ ┴ ┴
772 (h : is_O f (λ x, c * g x) l) :
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
773 is_O f g l :=
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
doc └──┘
774 let ⟨c, cnonneg, hc⟩ := h.exists_nonneg in (hc.of_const_mul_right cnonneg).is_O
id └─┘ └─────┘ └┘ ┴└────────────┘ └─────────────────┘ └──┘
src └────────────┘ └─────────────────┘ └──┘
typ └─┘ └─────┘ └┘ ┴└────────────┘ └─────────────────┘ └──┘
775
776 theorem is_O_with.const_mul_right' {g : α → R} {u : units R} {c' : ℝ} (hc' : 0 ≤ c')
id ┴ ┴ └───┘ ┴ ┴ ┴ └┘
src └───┘ ┴ ┴
typ ┴ ┴ └───┘ ┴ ┴ ┴ └┘
777 (h : is_O_with c' f g l) :
id └───────┘ └┘ ┴ ┴ ┴
src └───────┘
typ └───────┘ └┘ ┴ ┴ ┴
doc └───────┘
778 is_O_with (c' * ∥(↑u⁻¹:R)∥) f (λ x, ↑u * g x) l :=
id └───────┘ └┘ ┴ ┴ ┴┴└┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
typ └───────┘ └┘ ┴ ┴ ┴┴└┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴ ┴ ┴
doc └───────┘
779 h.trans (is_O_with_self_const_mul' _ _ _) hc'
id ┴└────┘ └───────────────────────┘ └─┘
src └────┘ └───────────────────────┘
typ ┴└────┘ └───────────────────────┘ └─┘
780
781 theorem is_O_with.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0)
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
782 {c' : ℝ} (hc' : 0 ≤ c') (h : is_O_with c' f g l) :
id ┴ ┴ └┘ └───────┘ └┘ ┴ ┴ ┴
src ┴ ┴ └───────┘
typ ┴ ┴ └┘ └───────┘ └┘ ┴ ┴ ┴
doc └───────┘
783 is_O_with (c' * ∥c∥⁻¹) f (λ x, c * g x) l :=
id └───────┘ └┘ ┴ ┴┴┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴└┘ ┴
typ └───────┘ └┘ ┴ ┴┴┴└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └───────┘
784 h.trans (is_O_with_self_const_mul c hc g l) hc'
id ┴└────┘ └──────────────────────┘ ┴ └┘ ┴ ┴ └─┘
src └────┘ └──────────────────────┘
typ ┴└────┘ └──────────────────────┘ ┴ └┘ ┴ ┴ └─┘
785
786 theorem is_O.const_mul_right' {g : α → R} {c : R} (hc : is_unit c) (h : is_O f g l) :
id ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴
src └─────┘ └──┘
typ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴
doc └─────┘ └──┘
787 is_O f (λ x, c * g x) l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
788 h.trans (is_O_self_const_mul' hc g l)
id ┴└────┘ └──────────────────┘ └┘ ┴ ┴
src └────┘ └──────────────────┘
typ ┴└────┘ └──────────────────┘ └┘ ┴ ┴
789
790 theorem is_O.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : is_O f g l) :
id ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
791 is_O f (λ x, c * g x) l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
792 h.const_mul_right' $ is_unit.mk0 c hc
id ┴└───────────────┘ └─────────┘ ┴ └┘
src └───────────────┘ └─────────┘
typ ┴└───────────────┘ └─────────┘ ┴ └┘
793
794 theorem is_O_const_mul_right_iff' {g : α → R} {c : R} (hc : is_unit c) :
id ┴ ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
795 is_O f (λ x, c * g x) l ↔ is_O f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
796 ⟨λ h, h.of_const_mul_right, λ h, h.const_mul_right' hc⟩
id ┴ ┴└─────────────────┘ ┴ ┴└───────────────┘ └┘
src └─────────────────┘ └───────────────┘
typ ┴ ┴└─────────────────┘ ┴ ┴└───────────────┘ └┘
797
798 theorem is_O_const_mul_right_iff {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
799 is_O f (λ x, c * g x) l ↔ is_O f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
800 is_O_const_mul_right_iff' $ is_unit.mk0 c hc
id └───────────────────────┘ └─────────┘ ┴ └┘
src └───────────────────────┘ └─────────┘
typ └───────────────────────┘ └─────────┘ ┴ └┘
801
802 theorem is_o.of_const_mul_right {g : α → R} {c : R} (h : is_o f (λ x, c * g x) l) :
id ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
803 is_o f g l :=
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
doc └──┘
804 h.trans_is_O (is_O_const_mul_self c g l)
id ┴└─────────┘ └─────────────────┘ ┴ ┴ ┴
src └─────────┘ └─────────────────┘
typ ┴└─────────┘ └─────────────────┘ ┴ ┴ ┴
805
806 theorem is_o.const_mul_right' {g : α → R} {c : R} (hc : is_unit c) (h : is_o f g l) :
id ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴
src └─────┘ └──┘
typ ┴ ┴ ┴ └─────┘ ┴ └──┘ ┴ ┴ ┴
doc └─────┘ └──┘
807 is_o f (λ x, c * g x) l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
808 h.trans_is_O (is_O_self_const_mul' hc g l)
id ┴└─────────┘ └──────────────────┘ └┘ ┴ ┴
src └─────────┘ └──────────────────┘
typ ┴└─────────┘ └──────────────────┘ └┘ ┴ ┴
809
810 theorem is_o.const_mul_right {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) (h : is_o f g l) :
id ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src ┴ └──┘
typ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘
811 is_o f (λ x, c * g x) l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
812 h.const_mul_right' $ is_unit.mk0 c hc
id ┴└───────────────┘ └─────────┘ ┴ └┘
src └───────────────┘ └─────────┘
typ ┴└───────────────┘ └─────────┘ ┴ └┘
813
814 theorem is_o_const_mul_right_iff' {g : α → R} {c : R} (hc : is_unit c) :
id ┴ ┴ ┴ └─────┘ ┴
src └─────┘
typ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
815 is_o f (λ x, c * g x) l ↔ is_o f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
816 ⟨λ h, h.of_const_mul_right, λ h, h.const_mul_right' hc⟩
id ┴ ┴└─────────────────┘ ┴ ┴└───────────────┘ └┘
src └─────────────────┘ └───────────────┘
typ ┴ ┴└─────────────────┘ ┴ ┴└───────────────┘ └┘
817
818 theorem is_o_const_mul_right_iff {g : α → 𝕜} {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
819 is_o f (λ x, c * g x) l ↔ is_o f g l :=
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └──┘ └──┘
820 is_o_const_mul_right_iff' $ is_unit.mk0 c hc
id └───────────────────────┘ └─────────┘ ┴ └┘
src └───────────────────────┘ └─────────┘
typ └───────────────────────┘ └─────────┘ ┴ └┘
821
822 /-! ### Multiplication -/
823
824 theorem is_O_with.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} {c₁ c₂ : ℝ}
id ┴ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴ ┴ ┴
825 (h₁ : is_O_with c₁ f₁ g₁ l) (h₂ : is_O_with c₂ f₂ g₂ l) :
id └───────┘ └┘ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
src └───────┘ └───────┘
typ └───────┘ └┘ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
doc └───────┘ └───────┘
826 is_O_with (c₁ * c₂) (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id └───────┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └───────┘
827 begin
st └─────
828 filter_upwards [h₁, h₂], simp only [mem_set_of_eq],
id └───────────┘
src └──────────────┘ └┘ ┴ └─────────┘└───────────┘┴
typ └──────────────┘ └┘ ┴ └─────────┘└───────────┘┴
doc └──────────────┘ └┘ ┴ └─────────┘ ┴
txt └──────────────┘ └┘ ┴ └─────────┘ ┴
par └──────────────┘ └┘ ┴ └─────────┘ ┴
pid └┘ └┘ ┴ ┴└──┘└┘ ┴
st ────────────────────────┘└─────────────────────────┘└─
829 intros x hx₁ hx₂,
src └──────────────┘
typ └──────────────┘
doc └──────────────┘
txt └──────────────┘
par └──────────────┘
pid └────────┘
st ─────────────────┘└─
830 apply le_trans (norm_mul_le _ _),
id └──────┘ └─────────┘
src └────┘└──────┘┴ └─────────┘└───┘
typ └────┘└──────┘┴ └─────────┘└───┘
doc └────┘ ┴ └───┘
txt └────┘ ┴ └───┘
par └────┘ ┴ └───┘
pid ┴ ┴ └───┘
st ─────────────────────────────────┘└─
831 convert mul_le_mul hx₁ hx₂ (norm_nonneg _) (le_trans (norm_nonneg _) hx₁) using 1,
id └────────┘ └─┘ └──────┘ └─────────┘ └─┘
src └──────┘└────────┘┴ ┴ ┴ └──┘ └──────┘┴ └─────────┘└──┘ └───────┘
typ └──────┘└────────┘┴ ┴└─┘┴ └──┘ └──────┘┴ └─────────┘└──┘└─┘└───────┘
doc └──────┘ ┴ ┴ ┴ └──┘ ┴ └──┘ └───────┘
txt └──────┘ ┴ ┴ ┴ └──┘ ┴ └──┘ └───────┘
par └──────┘ ┴ ┴ ┴ └──┘ ┴ └──┘ └───────┘
pid ┴ ┴ ┴ ┴ └──┘ ┴ └──┘ ┴└─────┘┴
st ──────────────────────────────────────────────────────────────────────────────────┘└─
832 rw normed_field.norm_mul,
id └───────────────────┘
src └─┘└───────────────────┘
typ └─┘└───────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────────────┘└─
833 ac_refl
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid ┴
st ─────────┘
834 end
st └─┘
835
836 theorem is_O.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
837 (h₁ : is_O f₁ g₁ l) (h₂ : is_O f₂ g₂ l) :
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
838 is_O (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
839 let ⟨c, hc⟩ := h₁, ⟨c', hc'⟩ := h₂ in (hc.mul hc').is_O
id └─┘ └┘ └┘ └─┘ └┘ └──┘ └──┘
src └──┘ └──┘
typ └─┘ └┘ └┘ └─┘ └┘ └──┘ └──┘
840
841 theorem is_O.mul_is_o {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
842 (h₁ : is_O f₁ g₁ l) (h₂ : is_o f₂ g₂ l) :
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
843 is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
844 begin
st └─────
845 intros c cpos,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────┘└─
846 rcases h₁.exists_pos with ⟨c', c'pos, hc'⟩,
id └───────────┘
src └─────┘└───────────┘└────────────────────┘
typ └─────┘└───────────┘└────────────────────┘
doc └─────┘ └────────────────────┘
txt └─────┘ └────────────────────┘
par └─────┘ └────────────────────┘
pid ┴ └────────────────────┘
st ───────────────────────────────────────────┘└─
847 exact (hc'.mul (h₂ (div_pos cpos c'pos))).congr_const (mul_div_cancel' _ (ne_of_gt c'pos))
id └─────┘ └┘ └─────┘ └──┘ └─────────────┘ └──────┘ └───┘
src └────┘ └─────┘┴ ┴ └─────┘┴ ┴ └──────────────┘ └─────────────┘└─┘ └──────┘┴ └─┘
typ └────┘ └─────┘┴ └┘┴ └─────┘┴└──┘┴ └──────────────┘ └─────────────┘└─┘ └──────┘┴└───┘└─┘
doc └────┘ ┴ ┴ ┴ ┴ └──────────────┘ └─┘ ┴ └─┘
txt └────┘ ┴ ┴ ┴ ┴ └──────────────┘ └─┘ ┴ └─┘
par └────┘ ┴ ┴ ┴ ┴ └──────────────┘ └─┘ ┴ └─┘
pid ┴ ┴ ┴ ┴ ┴ └──────────────┘ └─┘ ┴ └┘┴
st ────────────────────────────────────────────────────────────────────────────────────────────┘
848 end
st └─┘
849
850 theorem is_o.mul_is_O {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜}
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
851 (h₁ : is_o f₁ g₁ l) (h₂ : is_O f₂ g₂ l) :
id └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
852 is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
853 begin
st └─────
854 intros c cpos,
src └───────────┘
typ └───────────┘
doc └───────────┘
txt └───────────┘
par └───────────┘
pid └─────┘
st ──────────────┘└─
855 rcases h₂.exists_pos with ⟨c', c'pos, hc'⟩,
id └───────────┘
src └─────┘└───────────┘└────────────────────┘
typ └─────┘└───────────┘└────────────────────┘
doc └─────┘ └────────────────────┘
txt └─────┘ └────────────────────┘
par └─────┘ └────────────────────┘
pid ┴ └────────────────────┘
st ───────────────────────────────────────────┘└─
856 exact ((h₁ (div_pos cpos c'pos)).mul hc').congr_const (div_mul_cancel _ (ne_of_gt c'pos))
id └┘ └─────┘ └──┘ └─┘ └────────────┘ └──────┘ └───┘
src └────┘ ┴ └─────┘┴ ┴ └─────┘ └────────────┘ └────────────┘└─┘ └──────┘┴ └─┘
typ └────┘ └┘┴ └─────┘┴└──┘┴ └─────┘└─┘└────────────┘ └────────────┘└─┘ └──────┘┴└───┘└─┘
doc └────┘ ┴ ┴ ┴ └─────┘ └────────────┘ └─┘ ┴ └─┘
txt └────┘ ┴ ┴ ┴ └─────┘ └────────────┘ └─┘ ┴ └─┘
par └────┘ ┴ ┴ ┴ └─────┘ └────────────┘ └─┘ ┴ └─┘
pid ┴ ┴ ┴ ┴ └─────┘ └────────────┘ └─┘ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────────────────────────┘
857 end
st └─┘
858
859 theorem is_o.mul {f₁ f₂ : α → R} {g₁ g₂ : α → 𝕜} (h₁ : is_o f₁ g₁ l) (h₂ : is_o f₂ g₂ l) :
id ┴ ┴ ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ ┴ ┴ ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
860 is_o (λ x, f₁ x * f₂ x) (λ x, g₁ x * g₂ x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
861 h₁.mul_is_O h₂.is_O
id └┘└───────┘ └┘└───┘
src └───────┘ └───┘
typ └┘└───────┘ └┘└───┘
862
863 /-! ### Scalar multiplication -/
864
865 section smul_const
866 variables [normed_space 𝕜 E']
id └──────────┘
src └──────────┘
typ └──────────┘
doc └──────────┘
867
868 theorem is_O_with.const_smul_left (h : is_O_with c f' g l) (c' : 𝕜) :
id └───────┘ ┴ └┘ ┴ ┴ ┴
src └───────┘
typ └───────┘ ┴ └┘ ┴ ┴ ┴
doc └───────┘
869 is_O_with (∥c'∥ * c) (λ x, c' • f' x) g l :=
id └───────┘ ┴└┘┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴ ┴
typ └───────┘ ┴└┘┴ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ ┴
doc └───────┘
870 by refine ((h.norm_left.const_mul_left (∥c'∥)).congr _ _ (λ _, rfl)).of_norm_left;
id └────────────────────────┘ ┴└┘┴ └─┘
src └─────┘ └────────────────────────┘┴ ┴ ┴└───────────┘ └──┘└─┘└─────────────┘
typ └─────┘ └────────────────────────┘┴ ┴└┘┴└───────────┘ └──┘└─┘└─────────────┘
doc └─────┘ └────────────────────────┘┴ └───────────┘ └──┘ └─────────────┘
txt └─────┘ ┴ └───────────┘ └──┘ └─────────────┘
par └─────┘ ┴ └───────────┘ └──┘ └─────────────┘
pid ┴ ┴ └───────────┘ └──┘ └────────────┘┴
st └────────────────────────────────────────────────────────────────────────────────
871 intros; simp only [norm_norm, norm_smul]
id └───────┘ └───────┘
src └────┘ └─────────┘└───────┘└┘└───────┘└─
typ └────┘ └─────────┘└───────┘└┘└───────┘└─
doc └────┘ └─────────┘ └┘ └─
txt └────┘ └─────────┘ └┘ └─
par └────┘ └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st ─────────────────────────────────────────────
872
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
873 theorem is_O_const_smul_left_iff {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
874 is_O (λ x, c • f' x) g l ↔ is_O f' g l :=
id └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘
875 begin
st └─────
876 have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id ┴┴┴ ┴ └┘ └──────────┘ └┘
src └──────────┘┴ ┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘
typ └──────────┘┴┴┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘└┘
doc └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
txt └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
par └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
pid └───────┘└─┘ ┴ ┴┴ └───┘ ┴ └─────┘
st ────────────────────┘└──────────────────────────────┘└─
877 rw [←is_O_norm_left], simp only [norm_smul],
id └────────────┘ └───────┘
src └───┘└────────────┘┴ └─────────┘└───────┘┴
typ └───┘└────────────┘┴ └─────────┘└───────┘┴
doc └───┘ ┴ └─────────┘ ┴
txt └───┘ ┴ └─────────┘ ┴
par └───┘ ┴ └─────────┘ ┴
pid └─┘ ┴ ┴└──┘└┘ ┴
st ────────────────────┘└──────────────────────┘└─
878 rw [is_O_const_mul_left_iff cne0, is_O_norm_left],
id └─────────────────────┘ └──┘ └────────────┘
src └──┘└─────────────────────┘┴ └┘└────────────┘┴
typ └──┘└─────────────────────┘┴└──┘└┘└────────────┘┴
doc └──┘ ┴ └┘ ┴
txt └──┘ ┴ └┘ ┴
par └──┘ ┴ └┘ ┴
pid └┘ ┴ └┘ ┴
st ─────────────────────────────────┘└──────────────┘└──
879 end
st ──┘
880
881 theorem is_o_const_smul_left (h : is_o f' g l) (c : 𝕜) :
id └──┘ └┘ ┴ ┴ ┴
src └──┘
typ └──┘ └┘ ┴ ┴ ┴
doc └──┘
882 is_o (λ x, c • f' x) g l :=
id └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴
doc └──┘
883 begin
st └─────
884 refine ((h.norm_left.const_mul_left (∥c∥)).congr_left _).of_norm_left,
id └────────────────────────┘ ┴┴┴
src └─────┘ └────────────────────────┘┴ ┴ ┴└───────────────────────────┘
typ └─────┘ └────────────────────────┘┴ ┴┴┴└───────────────────────────┘
doc └─────┘ └────────────────────────┘┴ └───────────────────────────┘
txt └─────┘ ┴ └───────────────────────────┘
par └─────┘ ┴ └───────────────────────────┘
pid ┴ ┴ └──────────────────────────┘┴
st ──────────────────────────────────────────────────────────────────────┘└─
885 exact λ x, (norm_smul _ _).symm
id └───────┘
src └────┘ └──┘ └───────┘└─────────┘
typ └────┘ └──┘ └───────┘└─────────┘
doc └────┘ └──┘ └─────────┘
txt └────┘ └──┘ └─────────┘
par └────┘ └──┘ └─────────┘
pid ┴ └──┘ └───────┘└┘
st ─────────────────────────────────┘
886 end
st └─┘
887
888 theorem is_o_const_smul_left_iff {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
889 is_o (λ x, c • f' x) g l ↔ is_o f' g l :=
id └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └──┘ └┘ ┴ ┴
doc └──┘ └──┘
890 begin
st └─────
891 have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id ┴┴┴ ┴ └┘ └──────────┘ └┘
src └──────────┘┴ ┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘
typ └──────────┘┴┴┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘└┘
doc └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
txt └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
par └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
pid └───────┘└─┘ ┴ ┴┴ └───┘ ┴ └─────┘
st ────────────────────┘└──────────────────────────────┘└─
892 rw [←is_o_norm_left], simp only [norm_smul],
id └────────────┘ └───────┘
src └───┘└────────────┘┴ └─────────┘└───────┘┴
typ └───┘└────────────┘┴ └─────────┘└───────┘┴
doc └───┘ ┴ └─────────┘ ┴
txt └───┘ ┴ └─────────┘ ┴
par └───┘ ┴ └─────────┘ ┴
pid └─┘ ┴ ┴└──┘└┘ ┴
st ────────────────────┘└──────────────────────┘└─
893 rw [is_o_const_mul_left_iff cne0, is_o_norm_left]
id └─────────────────────┘ └──┘ └────────────┘
src └──┘└─────────────────────┘┴ └┘└────────────┘└┘
typ └──┘└─────────────────────┘┴└──┘└┘└────────────┘└┘
doc └──┘ ┴ └┘ └┘
txt └──┘ ┴ └┘ └┘
par └──┘ ┴ └┘ └┘
pid └┘ ┴ └┘ ┴┴
st ─────────────────────────────────┘└──────────────┘┴┴
894 end
st └─┘
895
896 theorem is_O_const_smul_right {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
897 is_O f (λ x, c • f' x) l ↔ is_O f f' l :=
id └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘
898 begin
st └─────
899 have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id ┴┴┴ ┴ └┘ └──────────┘ └┘
src └──────────┘┴ ┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘
typ └──────────┘┴┴┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘└┘
doc └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
txt └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
par └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
pid └───────┘└─┘ ┴ ┴┴ └───┘ ┴ └─────┘
st ────────────────────┘└──────────────────────────────┘└─
900 rw [←is_O_norm_right], simp only [norm_smul],
id └─────────────┘ └───────┘
src └───┘└─────────────┘┴ └─────────┘└───────┘┴
typ └───┘└─────────────┘┴ └─────────┘└───────┘┴
doc └───┘ ┴ └─────────┘ ┴
txt └───┘ ┴ └─────────┘ ┴
par └───┘ ┴ └─────────┘ ┴
pid └─┘ ┴ ┴└──┘└┘ ┴
st ─────────────────────┘└──────────────────────┘└─
901 rw [is_O_const_mul_right_iff cne0, is_O_norm_right]
id └──────────────────────┘ └──┘ └─────────────┘
src └──┘└──────────────────────┘┴ └┘└─────────────┘└┘
typ └──┘└──────────────────────┘┴└──┘└┘└─────────────┘└┘
doc └──┘ ┴ └┘ └┘
txt └──┘ ┴ └┘ └┘
par └──┘ ┴ └┘ └┘
pid └┘ ┴ └┘ ┴┴
st ──────────────────────────────────┘└───────────────┘┴┴
902 end
st └─┘
903
904 theorem is_o_const_smul_right {c : 𝕜} (hc : c ≠ 0) :
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
905 is_o f (λ x, c • f' x) l ↔ is_o f f' l :=
id └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
src └──┘ ┴ ┴ └──┘
typ └──┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──┘ ┴ └┘ ┴
doc └──┘ └──┘
906 begin
st └─────
907 have cne0 : ∥c∥ ≠ 0, from mt (norm_eq_zero _).mp hc,
id ┴┴┴ ┴ └┘ └──────────┘ └┘
src └──────────┘┴ ┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘
typ └──────────┘┴┴┴┴┴└┘ └───┘└┘┴ └──────────┘└─────┘└┘
doc └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
txt └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
par └──────────┘ ┴ └┘ └───┘ ┴ └─────┘
pid └───────┘└─┘ ┴ ┴┴ └───┘ ┴ └─────┘
st ────────────────────┘└──────────────────────────────┘└─
908 rw [←is_o_norm_right], simp only [norm_smul],
id └─────────────┘ └───────┘
src └───┘└─────────────┘┴ └─────────┘└───────┘┴
typ └───┘└─────────────┘┴ └─────────┘└───────┘┴
doc └───┘ ┴ └─────────┘ ┴
txt └───┘ ┴ └─────────┘ ┴
par └───┘ ┴ └─────────┘ ┴
pid └─┘ ┴ ┴└──┘└┘ ┴
st ─────────────────────┘└──────────────────────┘└─
909 rw [is_o_const_mul_right_iff cne0, is_o_norm_right]
id └──────────────────────┘ └──┘ └─────────────┘
src └──┘└──────────────────────┘┴ └┘└─────────────┘└┘
typ └──┘└──────────────────────┘┴└──┘└┘└─────────────┘└┘
doc └──┘ ┴ └┘ └┘
txt └──┘ ┴ └┘ └┘
par └──┘ ┴ └┘ └┘
pid └┘ ┴ └┘ ┴┴
st ──────────────────────────────────┘└───────────────┘┴┴
910 end
st └─┘
911
912 end smul_const
913
914 section smul
915
916 variables [normed_space 𝕜 E'] [normed_space 𝕜 F']
id └──────────┘ └──────────┘
src └──────────┘ └──────────┘
typ └──────────┘ └──────────┘
doc └──────────┘ └──────────┘
917
918 theorem is_O_with.smul {k₁ k₂ : α → 𝕜} (h₁ : is_O_with c k₁ k₂ l) (h₂ : is_O_with c' f' g' l) :
id ┴ ┴ └───────┘ ┴ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
src └───────┘ └───────┘
typ ┴ ┴ └───────┘ ┴ └┘ └┘ ┴ └───────┘ └┘ └┘ └┘ ┴
doc └───────┘ └───────┘
919 is_O_with (c * c') (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id └───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └───────┘
920 by refine ((h₁.norm_norm.mul h₂.norm_norm).congr rfl _ _).of_norm_norm;
id └──────────────┘ └──────────┘ └─┘
src └─────┘ └──────────────┘┴ └──────┘└─┘└────────────────┘
typ └─────┘ └──────────────┘┴└──────────┘└──────┘└─┘└────────────────┘
doc └─────┘ └──────────────┘┴└──────────┘└──────┘ └────────────────┘
txt └─────┘ ┴ └──────┘ └────────────────┘
par └─────┘ ┴ └──────┘ └────────────────┘
pid ┴ ┴ └──────┘ └───────────────┘┴
st └─────────────────────────────────────────────────────────────────────
921 by intros; simp only [norm_smul]
id └───────┘
src └────┘ └─────────┘└───────┘└─
typ └────┘ └─────────┘└───────┘└─
doc └────┘ └─────────┘ └─
txt └────┘ └─────────┘ └─
par └────┘ └─────────┘ └─
pid ┴└──┘└┘ ┴└
st ───────────────────────────────────
922
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
923 theorem is_O.smul {k₁ k₂ : α → 𝕜} (h₁ : is_O k₁ k₂ l) (h₂ : is_O f' g' l) :
id ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
924 is_O (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
925 by refine ((h₁.norm_norm.mul h₂.norm_norm).congr _ _).of_norm_norm;
id └──────────────┘ └──────────┘
src └─────┘ └──────────────┘┴ └───────────────────────┘
typ └─────┘ └──────────────┘┴└──────────┘└───────────────────────┘
doc └─────┘ └──────────────┘┴└──────────┘└───────────────────────┘
txt └─────┘ ┴ └───────────────────────┘
par └─────┘ ┴ └───────────────────────┘
pid ┴ ┴ └──────────────────────┘┴
st └─────────────────────────────────────────────────────────────────
926 by intros; simp only [norm_smul]
id └───────┘
src └────┘ └─────────┘└───────┘└─
typ └────┘ └─────────┘└───────┘└─
doc └────┘ └─────────┘ └─
txt └────┘ └─────────┘ └─
par └────┘ └─────────┘ └─
pid ┴└──┘└┘ ┴└
st ───────────────────────────────────
927
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
928 theorem is_O.smul_is_o {k₁ k₂ : α → 𝕜} (h₁ : is_O k₁ k₂ l) (h₂ : is_o f' g' l) :
id ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
929 is_o (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
930 by refine ((h₁.norm_norm.mul_is_o h₂.norm_norm).congr _ _).of_norm_norm;
id └───────────────────┘ └──────────┘
src └─────┘ └───────────────────┘┴ └───────────────────────┘
typ └─────┘ └───────────────────┘┴└──────────┘└───────────────────────┘
doc └─────┘ └───────────────────┘┴└──────────┘└───────────────────────┘
txt └─────┘ ┴ └───────────────────────┘
par └─────┘ ┴ └───────────────────────┘
pid ┴ ┴ └──────────────────────┘┴
st └──────────────────────────────────────────────────────────────────────
931 by intros; simp only [norm_smul]
id └───────┘
src └────┘ └─────────┘└───────┘└─
typ └────┘ └─────────┘└───────┘└─
doc └────┘ └─────────┘ └─
txt └────┘ └─────────┘ └─
par └────┘ └─────────┘ └─
pid ┴└──┘└┘ ┴└
st ───────────────────────────────────
932
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
933 theorem is_o.smul_is_O {k₁ k₂ : α → 𝕜} (h₁ : is_o k₁ k₂ l) (h₂ : is_O f' g' l) :
id ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
934 is_o (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
935 by refine ((h₁.norm_norm.mul_is_O h₂.norm_norm).congr _ _).of_norm_norm;
id └───────────────────┘ └──────────┘
src └─────┘ └───────────────────┘┴ └───────────────────────┘
typ └─────┘ └───────────────────┘┴└──────────┘└───────────────────────┘
doc └─────┘ └───────────────────┘┴└──────────┘└───────────────────────┘
txt └─────┘ ┴ └───────────────────────┘
par └─────┘ ┴ └───────────────────────┘
pid ┴ ┴ └──────────────────────┘┴
st └──────────────────────────────────────────────────────────────────────
936 by intros; simp only [norm_smul]
id └───────┘
src └────┘ └─────────┘└───────┘└─
typ └────┘ └─────────┘└───────┘└─
doc └────┘ └─────────┘ └─
txt └────┘ └─────────┘ └─
par └────┘ └─────────┘ └─
pid ┴└──┘└┘ ┴└
st ───────────────────────────────────
937
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
938 theorem is_o.smul {k₁ k₂ : α → 𝕜} (h₁ : is_o k₁ k₂ l) (h₂ : is_o f' g' l) :
id ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
src └──┘ └──┘
typ ┴ ┴ └──┘ └┘ └┘ ┴ └──┘ └┘ └┘ ┴
doc └──┘ └──┘
939 is_o (λ x, k₁ x • f' x) (λ x, k₂ x • g' x) l :=
id └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └──┘
940 by refine ((h₁.norm_norm.mul h₂.norm_norm).congr _ _).of_norm_norm;
id └──────────────┘ └──────────┘
src └─────┘ └──────────────┘┴ └───────────────────────┘
typ └─────┘ └──────────────┘┴└──────────┘└───────────────────────┘
doc └─────┘ └──────────────┘┴└──────────┘└───────────────────────┘
txt └─────┘ ┴ └───────────────────────┘
par └─────┘ ┴ └───────────────────────┘
pid ┴ ┴ └──────────────────────┘┴
st └─────────────────────────────────────────────────────────────────
941 by intros; simp only [norm_smul]
id └───────┘
src └────┘ └─────────┘└───────┘└─
typ └────┘ └─────────┘└───────┘└─
doc └────┘ └─────────┘ └─
txt └────┘ └─────────┘ └─
par └────┘ └─────────┘ └─
pid ┴└──┘└┘ ┴└
st ───────────────────────────────────
942
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
943 end smul
944
945 /-! ### Relation between `f = o(g)` and `f / g → 0` -/
946
947 theorem is_o.tendsto_0 {f g : α → 𝕜} {l : filter α} (h : is_o f g l) :
id ┴ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴
src └────┘ └──┘
typ ┴ ┴ └────┘ ┴ └──┘ ┴ ┴ ┴
doc └──┘
948 tendsto (λ x, f x / (g x)) l (𝓝 0) :=
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────┘ ┴ ┴
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴
949 have eq₁ : is_o (λ x, f x / g x) (λ x, g x / g x) l,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
950 from h.mul_is_O (is_O_refl _ _),
id ┴└───────┘ └───────┘
src └───────┘ └───────┘
typ ┴└───────┘ └───────┘
951 have eq₂ : is_O (λ x, g x / g x) (λ x, (1 : 𝕜)) l,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
952 from is_O_of_le _ (λ x, by by_cases h : ∥g x∥ = 0; simp [h, zero_le_one]),
id └────────┘ ┴ ┴┴ ┴┴ ┴ ┴ └─────────┘
src └────────┘ └───────┘ └─┘┴ ┴ ┴┴┴└┘ └────┘ └┘└─────────┘┴
typ └────────┘ ┴ └───────┘ └─┘┴┴┴┴┴┴┴└┘ └────┘┴└┘└─────────┘┴
doc └───────┘ └─┘ ┴ ┴ └┘ └────┘ └┘ ┴
txt └───────┘ └─┘ ┴ ┴ └┘ └────┘ └┘ ┴
par └───────┘ └─┘ ┴ ┴ └┘ └────┘ └┘ ┴
pid ┴ └─┘ ┴ ┴ ┴┴ ┴┴ └┘ ┴
st └────────────────────────────────────────────┘
953 (is_o_one_iff 𝕜).mp (eq₁.trans_is_O eq₂)
id └──────────┘ ┴ └┘ └─┘└─────────┘ └─┘
src └──────────┘ └┘ └─────────┘
typ └──────────┘ ┴ └┘ └─┘└─────────┘ └─┘
954
955 private theorem is_o_of_tendsto {f g : α → 𝕜} {l : filter α}
id ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ └────┘ ┴
956 (hgf : ∀ x, g x = 0 → f x = 0) (h : tendsto (λ x, f x / (g x)) l (𝓝 0)) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ └─────┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────┘ ┴
957 is_o f g l :=
id └──┘ ┴ ┴ ┴
src └──┘
typ └──┘ ┴ ┴ ┴
doc └──┘
958 have eq₁ : is_o (λ x, f x / (g x)) (λ x, (1 : 𝕜)) l,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
959 from (is_o_one_iff _).mpr h,
id └──────────┘ └─┘ ┴
src └──────────┘ └─┘
typ └──────────┘ └─┘ ┴
960 have eq₂ : is_o (λ x, f x / g x * g x) g l,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
961 by convert eq₁.mul_is_O (is_O_refl _ _); simp,
id └──────────┘ └───────┘
src └──────┘└──────────┘┴ └───────┘└───┘ └──┘
typ └──────┘└──────────┘┴ └───────┘└───┘ └──┘
doc └──────┘ ┴ └───┘ └──┘
txt └──────┘ ┴ └───┘ └──┘
par └──────┘ ┴ └───┘ └──┘
pid ┴ ┴ └───┘
st └─────────────────────────────────────────┘
962 have eq₃ : is_O f (λ x, f x / g x * g x) l,
id └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
963 begin
st └─────
964 refine is_O_of_le _ (λ x, _),
id └────────┘
src └─────┘└────────┘└─┘ └────┘
typ └─────┘└────────┘└─┘ └────┘
doc └─────┘ └─┘ └────┘
txt └─────┘ └─┘ └────┘
par └─────┘ └─┘ └────┘
pid ┴ └─┘ └────┘
st ───────────────────────────────┘└─
965 by_cases H : g x = 0,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴ ┴┴└┘
typ └───────┘ └─┘┴┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ ┴┴
st ───────────────────────┘└─
966 { simp only [H, hgf _ H, mul_zero] },
id ┴ └─┘ ┴ └──────┘
src └─────────┘ └┘ └─┘ └┘└──────┘└┘
typ └─────────┘┴└┘└─┘└─┘┴└┘└──────┘└┘
doc └─────────┘ └┘ └─┘ └┘ └┘
txt └─────────┘ └┘ └─┘ └┘ └┘
par └─────────┘ └┘ └─┘ └┘ └┘
pid ┴└──┘└┘ └┘ └─┘ └┘ ┴┴
st ─────┘└───────────────────────────────┘└┘└
967 { simp only [div_mul_cancel _ H] }
id └────────────┘ ┴
src └─────────┘└────────────┘└─┘ └┘
typ └─────────┘└────────────┘└─┘┴└┘
doc └─────────┘ └─┘ └┘
txt └─────────┘ └─┘ └┘
par └─────────┘ └─┘ └┘
pid ┴└──┘└┘ └─┘ ┴┴
st ────────────────────────────────────┘└─
968 end,
st ────┘
969 eq₃.trans_is_o eq₂
id └─┘└─────────┘ └─┘
src └─────────┘
typ └─┘└─────────┘ └─┘
970
971 theorem is_o_iff_tendsto {f g : α → 𝕜} {l : filter α}
id ┴ ┴ └────┘ ┴
src └────┘
typ ┴ ┴ └────┘ ┴
972 (hgf : ∀ x, g x = 0 → f x = 0) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
973 is_o f g l ↔ tendsto (λ x, f x / (g x)) l (𝓝 0) :=
id └──┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └──┘ ┴ └─────┘ ┴ ┴
typ └──┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘ └─────┘ ┴
974 iff.intro is_o.tendsto_0 (is_o_of_tendsto hgf)
id └───────┘ └────────────┘ └─────────────┘ └─┘
src └───────┘ └────────────┘ └─────────────┘
typ └───────┘ └────────────┘ └─────────────┘ └─┘
975
976 /-! ### Miscellanous lemmas -/
977
978 theorem is_o_pow_pow {m n : ℕ} (h : m < n) :
id ┴ ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴ ┴
979 is_o (λ(x : 𝕜), x^n) (λx, x^m) (𝓝 0) :=
id └──┘ ┴ ┴┴┴ ┴ ┴┴┴ ┴
src └──┘ ┴ ┴ ┴
typ └──┘ ┴ ┴┴┴ ┴ ┴┴┴ ┴
doc └──┘ ┴
980 begin
st └─────
981 let p := n - m,
id ┴ ┴ ┴
src └───────┘ ┴┴┴
typ └───────┘┴┴┴┴┴
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid └───┘┴└─┘ ┴ ┴
st ───────────────┘└─
982 have nmp : n = m + p := (nat.add_sub_cancel' (le_of_lt h)).symm,
id ┴ ┴ ┴ ┴ ┴ └─────────────────┘ └──────┘ ┴
src └─────────┘ ┴┴┴ ┴┴┴ └──┘ └─────────────────┘┴ └──────┘┴ └─────┘
typ └─────────┘┴┴┴┴┴┴┴┴┴└──┘ └─────────────────┘┴ └──────┘┴┴└─────┘
doc └─────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────┘
txt └─────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────┘
par └─────────┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └─────┘
pid └──────┘└─┘ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └────┘┴
st ────────────────────────────────────────────────────────────────┘└─
983 have : (λ(x : 𝕜), x^m) = (λx, x^m * 1), by simp only [mul_one],
id ┴ ┴ ┴ ┴ └─────┘
src └─────┘ └───┘ └─┘ ┴ └┘ ┴ └─┘ ┴┴└─┘ └─────────┘└─────┘┴
typ └─────┘ └───┘┴└─┘ ┴ └┘ ┴ └─┘ ┴┴┴└─┘ └─────────┘└─────┘┴
doc └─────┘ └───┘ └─┘ └┘ ┴ └─┘ ┴ └─┘ └─────────┘ ┴
txt └─────┘ └───┘ └─┘ └┘ ┴ └─┘ ┴ └─┘ └─────────┘ ┴
par └─────┘ └───┘ └─┘ └┘ ┴ └─┘ ┴ └─┘ └─────────┘ ┴
pid └───┘└┘ └───┘ └─┘ └┘ ┴ └─┘ ┴ └─┘ ┴└──┘└┘ ┴
st ───────────────────────────────────────┘ └─
984 simp only [this, pow_add, nmp],
id └──┘ └─────┘ └─┘
src └─────────┘ └┘└─────┘└┘ ┴
typ └─────────┘└──┘└┘└─────┘└┘└─┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st ───────────────────────────────┘└─
985 refine is_O.mul_is_o (is_O_refl _ _) ((is_o_one_iff _).2 _),
id └───────────┘ └───────┘ └──────────┘
src └─────┘└───────────┘┴ └───────┘└────┘ └──────────┘└──────┘
typ └─────┘└───────────┘┴ └───────┘└────┘ └──────────┘└──────┘
doc └─────┘ ┴ └────┘ └──────┘
txt └─────┘ ┴ └────┘ └──────┘
par └─────┘ ┴ └────┘ └──────┘
pid ┴ ┴ └────┘ └──────┘
st ────────────────────────────────────────────────────────────┘└─
986 convert (continuous_pow p).tendsto (0 : 𝕜),
id └────────────┘ ┴ ┴
src └──────┘ └────────────┘┴ └────────┘ └──┘ ┴
typ └──────┘ └────────────┘┴┴└────────┘ └──┘┴┴
doc └──────┘ ┴ └────────┘ └──┘ ┴
txt └──────┘ ┴ └────────┘ └──┘ ┴
par └──────┘ ┴ └────────┘ └──┘ ┴
pid ┴ ┴ └────────┘ └──┘ ┴
st ───────────────────────────────────────────┘└─
987 exact (zero_pow (nat.sub_pos_of_lt h)).symm
id └──────┘ └───────────────┘ ┴
src └────┘ └──────┘┴ └───────────────┘┴ └──────┘
typ └────┘ └──────┘┴ └───────────────┘┴┴└──────┘
doc └────┘ ┴ ┴ └──────┘
txt └────┘ ┴ ┴ └──────┘
par └────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └────┘└┘
st ─────────────────────────────────────────────┘
988 end
st └─┘
989
990 theorem is_o_pow_id {n : ℕ} (h : 1 < n) :
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
991 is_o (λ(x : 𝕜), x^n) (λx, x) (𝓝 0) :=
id └──┘ ┴ ┴┴┴ ┴ ┴ ┴
src └──┘ ┴ ┴
typ └──┘ ┴ ┴┴┴ ┴ ┴ ┴
doc └──┘ ┴
992 by { convert is_o_pow_pow h, simp only [pow_one] }
id └──────────┘ ┴ └─────┘
src └──────┘└──────────┘┴ └─────────┘└─────┘└┘
typ └──────┘└──────────┘┴┴ └─────────┘└─────┘└┘
doc └──────┘ ┴ └─────────┘ └┘
txt └──────┘ ┴ └─────────┘ └┘
par └──────┘ ┴ └─────────┘ └┘
pid ┴ ┴ ┴└──┘└┘ ┴┴
st └───────────────────────┘└────────────────────┘└┘
993
994 theorem is_O_with.right_le_sub_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c f₁ f₂ l) (hc : c < 1) :
id ┴ └┘ └───────┘ ┴ └┘ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ ┴ └┘ └───────┘ ┴ └┘ └┘ ┴ ┴ ┴
doc └───────┘
995 is_O_with (1 / (1 - c)) f₂ (λx, f₂ x - f₁ x) l :=
id └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └───────┘
996 mem_sets_of_superset h $ λ x hx,
id └──────────────────┘ ┴ ┴ └┘
src └──────────────────┘
typ └──────────────────┘ ┴ ┴ └┘
997 begin
st └─────
998 simp only [mem_set_of_eq] at hx ⊢,
id └───────────┘
src └─────────┘└───────────┘└───────┘
typ └─────────┘└───────────┘└───────┘
doc └─────────┘ └───────┘
txt └─────────┘ └───────┘
par └─────────┘ └───────┘
pid ┴└──┘└┘ ┴┴└─────┘
st ──────────────────────────────────┘└─
999 rw [mul_comm, one_div_eq_inv, ← div_eq_mul_inv, le_div_iff, mul_sub, mul_one, mul_comm],
id └──────┘ └────────────┘ └────────────┘ └────────┘ └─────┘ └─────┘ └──────┘
src └──┘└──────┘└┘└────────────┘└──┘└────────────┘└┘└────────┘└┘└─────┘└┘└─────┘└┘└──────┘┴
typ └──┘└──────┘└┘└────────────┘└──┘└────────────┘└┘└────────┘└┘└─────┘└┘└─────┘└┘└──────┘┴
doc └──┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └──┘ └┘ └┘ └┘ └┘ ┴
st ─────────────┘└──────────────┘└────────────────┘└──────────┘└───────┘└───────┘└────────┘└──
1000 { exact le_trans (sub_le_sub_left hx _) (norm_sub_norm_le _ _) },
id └──────┘ └─────────────┘ └┘ └──────────────┘
src └────┘└──────┘┴ └─────────────┘┴ └──┘ └──────────────┘└────┘
typ └────┘└──────┘┴ └─────────────┘┴└┘└──┘ └──────────────┘└────┘
doc └────┘ ┴ ┴ └──┘ └────┘
txt └────┘ ┴ ┴ └──┘ └────┘
par └────┘ ┴ ┴ └──┘ └────┘
pid ┴ ┴ ┴ └──┘ └───┘┴
st ───┘└───────────────────────────────────────────────────────────┘└┘└
1001 { exact sub_pos.2 hc }
id └─────┘ └┘
src └────┘└─────┘└─┘ ┴
typ └────┘└─────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ──────────────────────┘└─
1002 end
st ──┘
1003
1004 theorem is_O_with.right_le_add_of_lt_1 {f₁ f₂ : α → E'} (h : is_O_with c f₁ f₂ l) (hc : c < 1) :
id ┴ └┘ └───────┘ ┴ └┘ └┘ ┴ ┴ ┴
src └───────┘ ┴
typ ┴ └┘ └───────┘ ┴ └┘ └┘ ┴ ┴ ┴
doc └───────┘
1005 is_O_with (1 / (1 - c)) f₂ (λx, f₁ x + f₂ x) l :=
id └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ └┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴
doc └───────┘
1006 (h.neg_right.right_le_sub_of_lt_1 hc).neg_right.neg_left.congr rfl (λ x, neg_neg _)
id ┴└────────┘└───────────────────┘ └┘ └───────┘ └──────┘ └───┘ └─┘ ┴ └─────┘
src └───────────────────┘ └───┘ └─┘ └─────┘
typ ┴└────────┘└───────────────────┘ └┘ └───────┘ └──────┘ └───┘ └─┘ ┴ └─────┘
doc └────────┘ └───────┘ └──────┘
1007 (λ x, by rw [neg_sub, sub_neg_eq_add])
id ┴ └─────┘ └────────────┘
src └──┘└─────┘└┘└────────────┘┴
typ ┴ └──┘└─────┘└┘└────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └──────────┘└──────────────┘┴
1008
1009 end asymptotics